I recentely defended my PhD thesis under the supervision of Jérôme Feret in the Antique team at the ENS. I’m working to improve the Astrée static analyzer to be able to prove some security properties of an operating system. This implies to find ways to make the memory models of C and assembly to work together. Moreover, we need to be able to handle ghost variables to express complex properties inherent to low-level source code.


  • April 2023: I am chair of the SAS 2023 Artifact Evaluation Committee.
  • April 2022: I am chair of the SAS 2022 Artifact Evaluation Committee.
  • November 2020: I defended. See my defense.
  • April 2020: I am a member of the SAS 2020 Artifact Evaluation Committee.


  • Static Program Analysis
  • Abstract Interpretation
  • Formal Methods
  • Programming Languages
  • Compilers
  • Embedded Systems
  • Operating Systems
  • CPU architecture


  • PhD in Computer Science, 2020

    École Normale Supérieure

  • MSc in Computer Science, 2016

    École Normale Supérieure de Lyon/EPFL

  • BSc in Computer Science, 2014

    École Normale Supérieure de Lyon



Astrée for Security


Program Verification by Abstract Interpretation

A quick introduction to abstract interpretation


Proving the Security of Software-Intensive Embedded Systems by Abstract Interpretation

This thesis is dedicated to the analysis of low-level software, like operating systems, by abstract interpretation. Analyzing OSes is a …

Sharing Ghost Variables in a Collection of Abstract Domains

We propose a framework in which we share ghost variables across a collection of abstract domains allowing precise proofs of complex …



OCaml Print with style in your terminal using Format's semantic tags


OCaml Print aligned tables with mixed column sub-division


OCaml Python standard library in OCaml


Python Testing tool


Former intern