Léo Gourdin

Second year PhD student @ VERIMAG / TIMA laboratories

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

Research interests:


Formal methods; programming languages; type systems; compilation and optimizations; RISC-V and other open-hardware / modular ISA

Thesis subject:

Certifing compiler optimizations by symbolic execution modulo invariants (may change).
My advisors are S. Boulmé and F. Pétrot.

More specifically, I would like to demonstrate the capabilities of translation validation to validate multiple local (i.e. limited to [basic|super|extended]-blocks of code) and global transformations using a single generic verifier, certified using the Coq proof assistant. Originally, such a verifier had been designed by C. Six to verify a superblock scheduling optimization, but we believe it can be generalized to support larger blocks, and more complex optimizations, as lazy code motion, CSE, strength-reduction, software-pipelining, ...


About me: