Before joining STAMP, I was a postdoc in the Celtique team of the IRISA laboratory, Rennes, France, working with David Pichardie on CompCertSSA, a formally verified C compiler. Before joining Celtique, I was a PhD student at CEA and CentraleSupélec, under the supervision of Pascale Le Gall and Nikolai Kosmatov.
My research interests include formal methods, programming languages and software safety. I am a regular and pleased user of the Coq proof assistant.
Postdoc in team STAMP (2020-...)
I am currently working on Jasmin, a compiler written in Coq used to write high-assurance and high-speed cyptography. Programs are written in the Jasmin language and compiled to assembly. Jasmin is a rather low-level language that lets users control the low-level details of their programs but also features high-level constructs to make their lives easier than if they wrote these programs directly in assembly.
In the past year, I worked on adapting the proof of one pass of the compiler following the addition of major features to the language and the compiler (in particular, internal functions and sub-arrays). This work has not been merged yet into the main branch, but it is available in a development branch. Currently, I am working on adding the ARM architecture as a supported target of the Jasmin compiler (only x86_64 is supported so far). A port to RISC-V is also ongoing in parallel.
Postdoc in team Celtique (2018-2020)
During my first postdoc, I worked on the formalization in CompCertSSA
of a liveness analysis due to
Boissinot et al.
(2008). This analysis, unlike traditional dataflow-based ones, does not
compute the whole liveness of a program at once,
but instead answers so-called liveness queries of the form
a live at program point
Another particularity of this
analysis is that it specifically targets programs under SSA form.
I also worked on strengthening the dominance test of CompCertSSA, since this was a requirement for the formalization of the liveness analysis.
PhD thesis (2015-2018)
During my PhD, I worked on program slicing as a tool for software verification. More precisely, the goal was to give a formal justification to program slicing in the presence of runtime errors. This is explained in more details here.
The second part of my PhD was based on an elegant theory of control dependence due to Danicic et al. (2011) (control dependence is one of the two pillars of program slicing). The contributions were a formalization of part of this theory in Coq, and the design of an algorithm optimizing the one described by Danicic et al. This algorithm was written and proved correct in the Why3 proof system. This is detailed here.
Introductory examples to Coq and Why3 can be found here.
- jean-christophe [dot] lechenet [at] inria [dot] fr