Depuis septembre 2018, je suis enseignant-chercheur à CentraleSupélec sur le campus de Rennes, au sein de l'équipe CIDRE.
Avant cela, de janvier 2017 à août 2018, j'ai effectué un post-doctorat dans l'équipe
FLINT à l'Université de
Yale.
Mes activités de recherche s'inscrivaient dans le
projet CertiKOS
dont le but est de construire un noyau de système d'exploitation
formellement vérifié.
J'ai effectué ma thèse de doctorat dans l'équipe Celtique à l'Université de Rennes 1, d'août 2013 à novembre 2016. Mes travaux de doctorat portaient sur la compilation formellement vérifiée de code C de bas niveau.
Centres d'intérêt
J'effectue ma recherche dans les domaines d'analyse de programmes, compilation, méthodes formelles et cybersécurité.
Publications
Journaux
- CompCertS: A Memory-Aware Verified C Compiler Using a Pointer as Integer Semantics
avec S. Blazy and F. Besson.
In Journal of Automated Reasoning (JAR'18), Springer 2018.
Springer link - A Verified CompCert Front-End for a Memory Model supporting Pointer Arithmetic and Uninitialised Data
avec S. Blazy and F. Besson.
In Journal of Automated Reasoning (JAR'17), pp 1-48, Springer 2017.
Conférences
- An abstract stack based approach to verified compositional compilation to machine code
avec Y. Wang et Z. Shao. [slides]
In Principles of Programming Languages (POPL'19). - CompCertS: A Memory-Aware Verified C Compiler using Pointer as Integer Semantics
avec S. Blazy and F. Besson. [slides]
In Interactive Theorem Proving (ITP'17), LNCS 10499, pp. 81-97, Springer 2017. - A Concrete Memory Model for CompCert
avec 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
avec S. Blazy and F. Besson. [slides]
In Asian Symposium on Programming Languages and Systems (APLAS'14), LNCS 8858, Springer 2014.
Enseignements
- Systèmes d'Exploitation (M1) 2018/2019
- Compilation (M2) 2018/2019
- Algorithmes et Complexité (L3) 2018/2019
- Cours d'introduction à Coq (niveau M2) 2018/2019
- APF: Algorithmique et Programmation Fonctionnelle (niveau L1): TPs (2014/2015 et 2015/2016) et TDs (2015/2016)
- ACF: Analyse et Conception Formelles (niveau M1): TPs (2014/2015 et 2015/2016)
- EVL: Étude des vulnérabilités des logiciels (niveau M2): TPs (2014/2015)