Abstract

CompCert is a formally verified compiler. “Formally verified” means that there is a mathematical proof that the execution of the source matches that of the assembly code, and this proof has been checked by a proof assistant (here, Coq). It however provided limited optimization. We have since then implemented a variety of optimizations (scheduling, strength reduction across loop iterations…) that significantly reduce the gap compared to GCC . We also implemented a back-end for the Kalray KVX VLIW manycore processor. I will discuss these optimizations, as well as our plans for security features and Rust compilation.

Bio: David Monniaux obtained his PhD in 2001 in Paris under Prof Patrick Cousot; his dissertation was on the static analysis of probabilistic programs by abstract interpretation. He then joined CNRS as a junior researcher and first worked on the Astrée static analyzer, still in Paris. In 2007 he transferred to VERIMAG in Grenoble, where he works on various aspects of program verification (decision procedures, abstract interpretation…). He now is a senior researcher at CNRS and an adjunct professor at École polytechnique.