Since January 2017, I am a postdoctoral associate in the
FLINT research group at Yale University.
My research concerns the CertiKOS
project, which aims at building a formally verified OS kernel.
I was a PhD student in the Celtique team at Université de Rennes 1 in France, from 2013 to 2016. My PhD work was about certified compilation of low-level programs.
Research Interests
My research interests cover the topics of static analysis of programs, low-level code and proof methods.
Publications
- CompCertS: A Memory-Aware Verified C Compiler using Pointer as Integer Semantics
with S. Blazy and F. Besson.
In Interactive Theorem Proving (ITP'17), LNCS 10499, pp. 81-97, Springer 2017. - A Verified CompCert Front-End for a Memory Model supporting Pointer Arithmetic and Uninitialised Data
with S. Blazy and F. Besson.
In Journal of Automated Reasoning (JAR'17), pp 1-48, Springer 2017. - A Concrete Memory Model for CompCert
with S. Blazy and F. Besson. [slides]
In Interactive Theorem Proving (ITP'15), LNCS 9236, Springer 2015. - A Precise and Abstract Memory Model for C using Symbolic Values
with S. Blazy and F. Besson. [slides]
In Asian Symposium on Programming Languages and Systems (APLAS'14), LNCS 8858, Springer 2014.
Teaching
- APF: Algorithmique et Programmation Fonctionnelle (level: L1): lab sessions (2014/2015 and 2015/2016) and travaux dirigés (2015/2016)
- ACF: Analyse et Conception Formelles (level: M1): lab sessions (2014/2015 and 2015/2016)
- EVL: Étude des vulnérabilités des logiciels (level: M2): lab sessions (2014/2015)