I am a CNRS researcher (chargé de recherche CNRS)
in Formal Methods
Paris-Saclay. My research interests belong to the
formal verification of software and to the design and
development of programming languages.
Before integrating that team,
- I was a postdoc at Max Plank Institute for
Software Systems (MPI-SWS) in
Dreyer's team, on
project. Our objective was to formalize the soundness
type system and prove that some particular Rust
libraries written using unsafe features do not break
the whole type system;
- I was a PhD student in computer
science at Inria, in
of Xavier Leroy.
I designed, developed and formally
a static analyzer based on abstract interpretation. I
defended successfully on 26th May 2016. My PhD thesis
is available here.
thesis prize of the GdR GPL (french research group
on programming and software engineering)!
I am searching for a M2 intern for the second semester of 2022/2023.
Here is an internship proposal on invariants and ghost code in Creusot.
Don't hesistate to contact me if interested!
I am interested in the formal verification of software, using different approaches:
- Xavier Denis, my PhD student, is
developing under my supervision Creusot,
a deductive verification tool for the Rust
- I participated to the development of
concurrent separation logic, within the Coq proof
- I participated to the development of two logics based
on Iris for proving concurrent programs with a weakly
consistent memory semantics. The first one, iRC11,
targets the C11 memory model. In
Mével my PhD student, developed Cosmo, which targets
the Multicore OCaml memory model.
- Together with collaborators, I used some of these
logics to build semantic models of the type system of
Rust: in a sequentially consistent setting, in a weakly
consistent setting, or for proving the correctness a
type-directed weakest-precondition computation.
- During my PhD thesis, together with my collaborators,
I used Coq to code and prove
a static analyzer based on abstract interpretation. The
program was written directly in the calculus of
construction and transformed into OCaml through Coq's
- I participated to the development of the formally
by writing its parser and by contributing to its
IEEE758-compliant floating-point support.
In addition, I am interested in the design and development
of programming languages and their support software:
- I am member of the development team of the OCaml
language. I am particularly interested in the
development of the runtime library.
- I developed a memory profiler for OCaml, which is now
integrated in the official OCaml distribution. Its
specificity is that it is statistical: it
randomly samples a few allocations only in order to make
it possible to get precise information on the memory
behavior of the program without degrading significantly
- I have helped the development
which makes it possible to interoperate Rust and OCaml code
- I have developed
for the C11 grammar, based on the LR(1)
technology. This turned out to be particularly
I am a member of
association since a few years now. I used to participate
to the organization of the
contest contest, which aims at popularizing computer
science for teenagers.