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:

Keywords

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, ...

Publications:

Formally Verified Superblock Scheduling, a CPP'22 paper, by Six, Gourdin, Boulmé, Monniaux, Fasse and Nardino.
Certifying assembly optimizations in Coq by symbolic execution with hash-consing, a CoqWorkshop 2021 abstract, by Gourdin and Boulmé.
Formally verified postpass scheduling with peephole optimization for AArch64, a short AFADL'21 paper, by Gourdin.

About me:

Phone: +33 6 49 10 19
Work: IMAG building, Université Grenoble Alpes
Resume

Links: