"Formal Validation of Intra-Procedural Transformations by Defensive Symbolic Simulation." The thesis was supervised by Sylvain Boulmé (VERIMAG) and Fédéric Pétrot (TIMA).
More specifically, my work aimed 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 investigated 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.
My thesis defense took 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
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]
