Léo Gourdin

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.

Research interests:

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):

About me: