PhD student @ VERIMAG / TIMA laboratories, UGA, Grenoble
PACSS team (Proofs and Code analysis for Safety and Security).
The prefered way to reach me is via email:
leo (dot) gourdin (at) univ-grenoble-alpes (dot) fr
[Announce:] My thesis defense will take place on December 12, 2023 at 9:30 a.m.
Formal methods; programming languages; type systems; compilation and optimizations; RISC-V and other open-hardware / modular ISA
Thesis subject: Formal Validation of Intra-Procedural Transformations by Defensive Symbolic Simulation.
My advisors are S. Boulmé (VERIMAG) and F. Pétrot (TIMA).
More specifically, my work aims at using translation validation to prove correct multiple local (i.e. limited to basic/super/extended blocks of code) and global (i.e. intra-procedural) transformations using a single generic verifier, certified using the Coq proof assistant. In particular, we investigate how Symbolic Execution (SE) combined with abstract invariants can help in defensively validating complex transformations such as code motion, strength-reduction, or software pipelining.
Our work is implemented in an open-source fork of CompCert named Chamois-CompCert, which I used as an object of study for my thesis.
Publications (from newest to oldest):
- "Formally Verifying Optimizations with Block Simulations", an OOPSLA'23 paper, by Gourdin, Bonneau, Boulmé, Monniaux, and Bérard. [HAL|DOI]
- "Testing a Formally Verified Compiler", a TAP'23 paper, by Monniaux, Gourdin, Boulmé, and Lebeltel. [HAL|DOI]
- "Lazy Code Transformations in a Formally Verified Compiler", an ICOOOLPS'23 paper, by Gourdin. [HAL|DOI]
- "Formally Verified Advanced Optimizations for RISC-V", a poster presented at the RISC-V Summit 2023 in Barcelona, Spain, by Monniaux, Boulmé, and Gourdin. [PDF|ABSTRACT]
- "Formally Verified Superblock Scheduling", a CPP'22 paper, by Six, Gourdin, Boulmé, Monniaux, Fasse and Nardino. [HAL|DOI]
- "Certifying assembly optimizations in Coq by symbolic execution with hash-consing", a CoqWorkshop'21 abstract, by Gourdin and Boulmé. [ABSTRACT|SLIDES|VIDEO (on YouTube)]
- "Formally verified postpass scheduling with peephole optimization for AArch64", a short AFADL'21 paper, by Gourdin. [PDF|WEBSITE]
- Phone: +33 6 49 10 19
- Work: IMAG building, Université Grenoble Alpes