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 interested in the formal verification of software, using different approaches:
- Xavier Denis, my PhD student, is
under my supervision a deductive verification tool for
- 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.