Postdoc in formal methods for control systems

L’ENAC, École Nationale de l’Aviation Civile, est la plus importante des Grandes Écoles ou universités aéronautiques en Europe. Elle forme à un spectre large de métiers : des ingénieurs ou des professionnels de haut niveau capables de concevoir et faire évoluer les systèmes aéronautiques et plus largement ceux du transport aérien ainsi que des pilotes de ligne, des contrôleurs aériens ou encore des techniciens aéronautiques.
Ses laboratoires de recherche sont à la pointe de l’innovation et travaillent activement en coopération avec des universités internationales de haut niveau pour un transport aérien toujours plus sûr, efficace et durable.

L’ENAC est un établissement public à caractère scientifique, culturel et professionnel – grand établissement (EPSCP-GE), sous tutelle de la DGAC (Direction Générale de l’Aviation Civile), Direction du Ministère de la Transition Écologique et Solidaire. L’ENAC comprend une direction générale localisée à Toulouse et 8 sites en France.

Pour soutenir sa dynamique en faveur de la promotion de la diversité, l’ENAC facilite l’accueil et l’intégration des travailleurs en situation de handicap.


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.