Jacques-Henri Jourdan

ACM Software System Award

France - 2021

CNRS, Laboratoire Méthodes Formelles

citation

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.

Press Release

2021 ACM Software System Award

Xavier Leroy, Collège de France; Sandrine Blazy, University of Rennes 1, IRISA; Zaynah Dargaye, Nomadic Labs; Jacques-Henri Jourdan, CNRS, Laboratoire Méthodes Formelles; Michael Schmidt, AbsInt Angewandte Informatik; Bernhard Schommer, Saarland University, and AbsInt Angewandte Informatik GmbH; and Jean-Baptiste Tristan, Boston College, receive the ACM Software System Award for the development of CompCert, the first practically useful optimizing compiler targeting multiple commercial architectures that has a complete, mechanically checked proof of its correctness.

CompCert, initiated in 2005, is a compiler for the C programming language and the first industrial-strength compiler with a mechanically checked proof of correctness. It can be used with most computer architectures including PowerPC, ARM, RISC-V and x86 (32 and 64 bits) architectures.

When it was introduced, CompCert represented a major advance over other production compilers, because it did not experience miscompilation issues since it is formally verified using machine-assisted mathematical proofs. The code it produces is proved to behave exactly as specified by the semantics of the source C program. This level of confidence in the correctness of the compilation process enables CompCert to meet the highest levels of software assurance.

Today, CompCert continues as a research project at Inria, the French National Institute for Research in Digital Science and Technology and is available under commercial and noncommercial licenses (source code openly available for noncommercial use). Other researchers build on CompCert, and multiple corporations use it for safety-critical applications.