An expert researcher in the field of formal verification for industrial embedded systems

Fondazione Bruno Kessler
September 12 2017
Position Type
Full Time
Organization Type

FBK is a private research institution based in Trento (Italy) and operating in different scientific fields and disciplines. As such, it has the role of keeping the Autonomous Province of Trento within the mainstream of international research. FBK is made up of seven research centre, whose activities and production are available at



The Embedded Systems Research Unit (ES Unit) of the Information and Communication Technology Center of the Bruno Kessler Foundation (FBK-irst), Trento, Italy consists of about 25 people, including researchers, post-docs, PhD students, and programmers. The Unit carries out research, tool development and technology transfer in the field of design and verification of embedded systems.


Current research directions include:

  • Satisfiability Modulo Theory, and its application to the verification of hardware, embedded critical software, and hybrid systems (StateFlow/Simulink, Verilog, C/C++, SystemC)

  • Model Based Planning and Scheduling of aerospace domains using model checking and satisfiability modulo theory techniques

  • Formal Requirements Analysis based on techniques for temporal logics  (consistency checking, vacuity detection, input determinism, cause-effect analysis, realizability and synthesis)

  • Model-based engineering and formal verification of aerospace systems using model checking techniques, on-board reasoning systems for autonomous vehicles using planning techniques;

  • Formal Safety Analysis, based on the integration of traditional techniques (e.g. Fault-tree analysis, FMEA) with symbolic verification techniques

More information about the ES Unit is available at .

The ES Unit has an opening for a PostDoc position in the field of formal verification for industrial embedded systems in the framework of several research and technology transfer projects. The successful candidate will be employed for a period of at least three years (with a trial period of 6 months). He/She will carry out research activities in the field of formal methods applied to the design and implementation of adaptive systems with critical safety and security requirements. In particular, the activities will focus on:

  • declarative languages for the specification of dynamic embedded systems

  • formal verification of hybrid systems with non-linear dynamics

  • formal verification tool development and integration within standard industrial design environments

  • contract-based framework for compositional verification of the system based on the properties of components

  • design and synthesis of monitors to ensure that local properties are satisfied

  • formal safety assessment

The candidate is expected to work in collaboration with other researchers, programmers, and students involved in the project.

Application deadline: October 2nd, 2017  



Candidates are required to submit their applications by filling in the online form at

Please make sure that your application includes the following attachments (pdf format):

  • Detailed CV

  • Cover Letter (explaining your motivation for this specific position)

  • 2 professional references (e-mails and/or phone numbers)


Please read the Guidelines for Selection before completing your application.

For further information or technical issues regarding the application, please contact the Human Resources Service at


Candidates who pass the preliminary curricula screening will be contacted shortly afterwards for an interview.

Non selected applicants will be notified of their exclusion at the end of the selection process.

Please note that FBK may contact shortlisted candidates within a period of 12 months, for the selection processes of similar vacancies.

For reasons of professional transparency, the name of the successful candidate will be published on the FBK website following acceptance of the position.

This job comes from a partnership with Science Magazine and Euraxess

More searches like this