The open research positions are in the field formal verification of complex control systems. The expected activities include:

  • the development of formal verification techniques and their integration in model-based design environments
  • model checking of control systems and their interaction with hybrid models of the physical plants
  • contract-based compositional reasoning
  • model-based safety analysis
  • fault detection and diagnosis
  • runtime verification
  • software development for tools such as nuXmv, OCRA, xSAP, Kratos, COMPASS, and TASTE
  • training support, and document generation for technology transfer.

The candidate is expected to work in collaboration with other researchers, programmers, and students involved in the ES Unit. Moreover, the candidate is expected to interact with industrial partners and partners of research projects.

Job Requirements 

The ideal candidate should have:

  • PhD in computer science, mathematics or electronic engineering or equivalent 3-years research experience;
  • Software development skills (preferably in C, Python, Matlab, C++, Java);
  • Ability to carry out an independent research program;
  • Ability to work in a collaborative environment and deliver in research and/or industrial projects;
  • Accuracy, proactivity and goal orientation;
  • Oral and written proficiency in English.

In depth previous experience in at least one of the following areas is required:

  • Model Checking or other formal verification techniques,
  • First-order logic and SMT solvers,
  • Formal analysis of hybrid systems,
  • Runtime verification,
  • Formal safety assessment and diagnosis,
  • Temporal Logics and Property Specification Languages.

Background knowledge and/or previous experience in the following areas will be considered favorably:

  • Automated test case generation,
  • Formal Specification and Analysis of Architectures,
  • Mathematical modelling and computer-based simulation.

Application page

Deadline: 21 Mar 2022

Contact: