Postdoc in formal methods for control systems

The recruited postdoctoral researcher will contribute to the ANR/NSF CAFEE project, an international collaboration aiming at bridging the gap between control theory and formal verification at code level. The project targets end-to-end guarantees, from high-level control design to embedded software implementation, with applications in safety-critical systems (e.g., aerospace, robotics).

The postdoctoral researcher will be primarily involved in the design, implementation, and evaluation of formal verification methods for control software, with a particular focus on optimization-based control algorithms and their implementation.

Main scientific objectives

• Develop formal and exhaustive verification techniques for control system software at code level.

• Bridge high-level control guarantees (e.g., stability, performance, convergence) with low-level implementation semantics (finite precision arithmetic, C code).

• Contribute to the development of an end-to-end verification toolchain, integrating modeling, proof generation, and code-level validation.

Core Research activities

• Formal verification of control algorithms at code level

  • Design static analysis and deductive verification techniques to prove system-level properties (stability, robustness, performance).

  • Develop methods to express control-theoretic properties (e.g., Lyapunov invariants) as program invariants.

  • Apply and extend tools such as Frama-C, SMT solvers, and theorem provers.

• Verification of optimization-based control algorithms

  • Formalize and verify convex optimization algorithms embedded in control loops.

  • Prove termination and convergence guarantees, including finite-time convergence.

  • Analyze numerical aspects such as discretization, linearization, and solver correctness.

• Handling numerical precision and implementation effects

  • Model and verify the impact of floating-point and fixed-point arithmetic on system behavior.

  • Develop methods to ensure correctness under finite-precision computation.

• Contribution to an end-to-end verification toolchain

  • Participate in the extension of toolchains such as CocoSim for combined modeling, code generation, and verification.

  • Integrate verification techniques across multiple abstraction levels (model → code → hardware).

• Experimental validation and case studies

  • Apply developed methods to realistic control systems (e.g., UAVs, embedded controllers, trajectory planning).

  • Evaluate scalability and applicability on representative benchmarks.

Collaboration and dissemination

• Collaborate closely with project partners at ENAC and the University of Michigan.

• Contribute to joint publications in top-tier venues in formal methods, control, and programming languages.

• Participate in project meetings, workshops, and international research exchanges.

• Optionally contribute to supervision of PhD students and teaching-related activities.

The position is part of a dynamic international collaboration between ENAC and the University of Michigan, combining expertise in automated verification and interactive theorem proving. The project offers a unique opportunity to contribute to cutting-edge research at the intersection of control systems, formal methods, and embedded software verification, with strong connections to industrial and aerospace applications.

We are seeking a highly motivated candidate with a strong interdisciplinary background at the interface of control theory and formal methods.

Requiered qualifications

• PhD degree in one or more of the following fields:

  • Control Theory

  • Computer Science (Formal Methods, Programming Languages, Verification)

  • Applied Mathematics (with strong relevance to the topic)

Technical expertise

• Strong background in control systems theory, including:

  • Lyapunov theory (especially for discrete-time systems)

  • Stability and robustness analysis

  • Familiarity with optimization-based control is a strong plus

• Solid knowledge of formal methods, including:

  • Deductive verification and/or static analysis

  • Experience with tools such as Frama-C, SMT solvers, or proof assistants

  • Understanding of program semantics and verification at code level

• Familiarity with at least some of the following topics is highly desirable:

  • Integral Quadratic Constraints (IQC)

  • Convex optimization and numerical algorithms

  • Floating-point or fixed-point arithmetic verification

  • Hybrid systems and cyber-physical systems

  • Signal Temporal Logic (STL) or temporal logics

Programming skills

• Strong programming experience in C/C++, Python, or similar languages

• Experience with formal verification tools or scientific computing environments

Research profile

• Proven ability to conduct independent research

• Strong publication record in top-tier conferences and/or journals in relevant fields (formal methods, control, programming languages, embedded systems)

Language and communication

• Fluency in English (spoken and written)

• Ability to work in an international and interdisciplinary research environment

Personnal skills

• Strong analytical and problem-solving abilities

• Ability to collaborate across disciplines (control theory and computer science)

• Autonomy, initiative, and scientific curiosity