I’m a third-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 that we named Barocq. The purpose of Barocq is to write system code (e.g. microkernel) and verify properties on that code using the Rocq/Coq Proof Assistant.

From April to June 2025, I was a visiting PhD student at KTH Royal Institute of Technology in Stockholm. I worked with Roberto Guanciale and Henrik Karlsson on the re-implementation of the S3K microkernel in Barocq.

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

Publications

  • Towards Verifiable System Code using a DSL Compiled to Efficient and Readable C Code, at LCTES’26.
    Clément Chavanon, Henrik Karlsson, Frédéric Besson, Sandrine Blazy, Roberto Guanciale.
    Proceedings of the 27th ACM SIGPLAN/SIGBED International Conference on Languages, Compilers, and Tools for Embedded Systems (LCTES 2026). [doi].

  • PfComp: A Verified Compiler for Packet Filtering Leveraging Binary Decision Diagrams, at CPP’24.
    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] [talk].

Teaching assistance

2025 - 2026

  • PRGC (Programmation de confiance - Trustworthy programming), L3 ISTIC, University of Rennes.
    Lecturer: Sandrine Blazy.
  • Programmation fonctionnelle - Functional programming, 3INFO, INSA Rennes.
    Lecturer: Frédéric Besson.

2024 - 2025

  • PRGC (Programmation de confiance - Trustworthy programming), L3 ISTIC, University of Rennes.
    Lecturer: Sandrine Blazy.
  • Programmation fonctionnelle - Functional programming, 3INFO, INSA Rennes.
    Lecturer: Frédéric Besson.

2023 - 2024

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