Welcome !

I am a CNRS researcher (chargé de recherche CNRS) in the VALS team, which is part of the Laboratoire de Recherche en Informatique of Université Paris Saclay

Before integrating that team,

• 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 Rust's type system and prove that some particular unsafe Rust code fragments 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 defended successfully on 26th May 2016.

Research interests

My research interests include formal verification of software. In particular, my PhD project lies exactly between abstract interpretation and the Coq proof assistant.

I am also interested in several subjects linked to programming languages: LR parsing, floating-point arithmetic, compilation...

PhD thesis

My PhD thesis is available here. Its title is "Verasco: a Formally Verified C Static Analyzer".

It received the 2016 thesis prize of the GdR GPL (french research group on programming and software engineering)!

Software

Vincent Laporte and I are the two main authors of the Verasco formally verified static analyzer. I have written the abstract interpreter, and most of the numerical abstract domain hierarchy.

I developed a statistical memory profiler for OCaml. It provides OCaml developers a flexible tool for understanding the memory behavior of an OCaml program with virtually no overhead. It can be used through the xxxx+statistical-memprof Opam switches.

I am an occasional contributor to the CompCert verified compiler. In particular, I am the initial author of its parser, and I contributed to its support of IEEE754-compliant floating-point numbers.

With my wife, we are the authors of a few R packages.

I was the teaching assistant for the course "Langages de programmation et compilation", at ENS with Jean-Christophe Filliâtre, years 2013/2014 and 2014/2015.

I have been one of the organizers of the Junior Seminar of Inria Paris

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.

I have been a member of hackEns, the hackerspace of ENS. I am still happy to do fun hacks with electronics or with my RepRap.