Welcome !

I am a CNRS researcher (chargé de recherche CNRS) in Formal Methods Laboratory (LMF) of Université Paris-Saclay. My research interests belong to the formal verification of software and to the design and development of programming languages.

Research interests

I am interested in the formal verification of software, using different approaches:

• I am member of the development team of Creusot, a deductive verification tool for the Rust programming language. I collaborate with the rest of the Creusot team, which includes:
  • Xavier Denis, my former PhD student,
  • Arnaud Golfouse, my current PhD student,
  • Armaël Guéneau, a researcher at Inria Saclay and co-advisort of Arnaud,
  • Laurent Schneider, Inria engineer,
  • other contributors to Creusot, some of which are very far from our lab.
• I participated to the development of the Iris concurrent separation logic, within the Coq proof assistant.
• 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 addition, Glen 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 correct Verasco, a static analyzer based on abstract interpretation. The program was written directly in the calculus of construction and transformed into OCaml through Coq's extraction mechanism.
• I participated to the development of the formally verified compiler Compcert, 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 its performances.
• I have helped the development of ocaml-interop which makes it possible to interoperate Rust and OCaml code
• I have developed a parser for the C11 grammar, based on the LR(1) technology. This turned out to be particularly subtle!

Teaching

• Together with Armaël Guéneau, I am the teacher of the advanced programming (programmation avancée) course at ENS Paris-Saclay.
• I am teaching the Rust part of the course of functional programming and type systems at the parisian master of research in computer science (MPRI).

Before my integration to the LMF laboratory

• I was a postdoc at Max Plank Institute for Software Systems (MPI-SWS) in Derek Dreyer's team, on the RustBelt project. Our objective was to formalize the soundness of Rust's 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 team Gallium, under the direction of Xavier Leroy. I designed, developed and formally verified Verasco, a static analyzer based on abstract interpretation. I defended successfully on 26th May 2016. My PhD thesis is available here. It received the 2016 thesis prize of the GdR GPL (french research group on programming and software engineering)!

Misc

I am a member of the France-IOI association since a few years now. I used to participate to the organization of the French Bebras contest contest, which aims at popularizing computer science for teenagers.