I’m a second-year PhD student in the EPICURE team at INRIA Rennes. My supervisors are Sandrine Blazy and Frédéric Besson.

I’m working on a formally verified compiler of a subset of Gallina to C. The purpose of this subset is to write system code (e.g. microkernel) and verify properties on that code using the Coq Proof Assistant.

Formerly, I was an intern in the same research team under the supervision of Frédéric Besson and Tristan Ninet. I worked on a verified compiler for a packet filtering language.

Publications

• PfComp: A Verified Compiler for Packet Filtering Leveraging Binary Decision Diagrams.
  Clément Chavanon, Frédéric Besson, Tristan Ninet.
  Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2024). [doi] [pdf].

Teaching assistance

2023 - 2024

• PRGC (Programmation de confiance - Trustworthy programming), L3 ISTIC, University of Rennes.
  Lecturer: Sandrine Blazy
• ACE (Algorithmique et Complexité - Algorithmics and Complexity Analysis), L1 ISTIC, University of Rennes.
  Lecturer: Thomas Genet
• Programmation fonctionnelle - Functional programming, 3INFO, INSA Rennes.
  Lecturer: Frédéric Besson