Research on the formal verification of reactive and real-time software, with a particular focus on combining program analysis, deductive techniques, and synchronous model checking.

I contribute to the development of Frama-C/Synchrone, a Frama-C plug-in that extracts synchronous Lustre models from reactive C programs for subsequent formal verification. My work involves symbolic program analysis, abstract interpretation, deductive verification techniques, and model checking.

This work led to the paper Modular Extraction of Lustre Models from C Reactive Programs using Frama-C, published in EMSOFT 2026 and the IEEE TCAD journal (to appear).

Designed and teach a course on software testing and validation for approximately 50 students in EPITA’s Embedded & Real-Time Systems specialization, at M1/M2 level for a total of around 25h/year.

The course covers functional and structural testing, fuzzing, static analysis, and formal verification, with an emphasis on the verification and validation of safety-critical software.

I also participate in student assessment and internship juries.

PhD research on the formal verification of temporal properties for safety-critical real-time applications based on logical time, conducted as a CIFRE collaboration between Université Côte d’Azur, the Inria KAIROS team, and Krono-Safe/Asterios Technologies.

The work established formal semantics for the industrial PsyC language by combining the Synchronous-Reactive and Logical Execution Time models into the Synchronous Logical Execution Time framework.

I developed a verification methodology based on translation to synchronous models (both Esterel and Lustre), and symbolic model checking, together with temporal abstractions reducing verification cost.

Worked on the development and verification of the Asterios real-time software toolchain, for safety-critical applications.

• Contributed to the PsyC compiler written in C++ and to the associated real-time kernel written in C, including fault and error management, and the support of non time-critical tasks.

• Designed and implemented formal verification techniques and an OCaml verification prototype for PsyC, using synchronous models and symbolic model checking.

• Contributed to a compiler validation toolchain written in Python, including parsing, graph analyses, and validation of generated implementation artifacts in an avionics certification context.

• Participated in HAZOP safety analyses of software features.

• Co-supervised 3 interns on topics including Lingua Franca to PsyC translation and randomized PsyC code generation, which led to the discovery of 9 defects in the Asterios toolchain.