Optimizations in a formally verified compiler

Add to your list(s) Download to your calendar using vCal

• David Monniaux, CNRS/VERIMAG and École Polytechnique
• Thursday 20 July 2023, 14:00-15:00
• FW11, Computer Laboratory.

If you have a question about this talk, please contact Jamie Vicary.

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.

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computing and Mathematics
• Department of Computer Science and Technology talks and seminars
• FW11, Computer Laboratory
• Interested Talks
• Logic and Semantics Seminar (Computer Laboratory)
• School of Technology
• Security-related talks
• Trust & Technology Initiative - interesting events
• bld31
• tcw57’s list
• yk373's list

Note that ex-directory lists are not shown.