France - 2021
University of Rennes 1, IRISA
For development of the first industrial-strength optimizing compiler that has been the subject of a complete, mechanically checked proof of correctness
CompCert is the first industrial-strength compiler with a mechanically checked proof of correctness. It is an optimizing compiler in which all optimizations are proved correct or validated. Prior to CompCert's development, it was widely assumed that building verified software beyond "toy" examples would be impossible. CompCert represents a quantum leap that made this a reality, with the code produced by it comparable in speed to state-of-the-art alternatives, at the cost of somewhat slower compilation times. In turn, the emergence of CompCert ushered a new age of verification, with applications to real-world settings as critical as Airbus aircraft.
The CompCert compiler targets multiple widely used, commercial architectures: PowerPC, ARM, RISC-V, and x86. It has provided a formal semantics for the C programming language, which has made it possible to formally reason about systems implemented for a multitude of settings and to extend the desired guarantees "down to the metal". In turn, this work has directly enabled researchers to develop a series of extensions that can themselves be considered foundational and has inspired highly successful community-wide programs such as DARPA's HACMS.