Xavier Leroy

Digital Library

ACM Software System Award

France - 2021

Collège de France

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

ACM Fellows

France - 2015

citation

For contributions to safe, high-performance functional programming languages and compilers, and to compiler verification.

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.

ACM Fellows Named For Computing Innovations That Are Advancing Technology In The Digital Age

ACM has recognized 42 of its members for their significant contributions to the development and application of computing in areas from data management and spoken-language processing to robotics and cryptography. The achievements of the 2015 ACM Fellows are fueling advances in computing that are driving the growth of the global digital economy.

"Whether they work in leading universities, corporations, or research laboratories, these newly minted ACM Fellows are responsible for the breakthroughs and industrial innovations that are transforming society at every level," explains ACM President Alexander L. Wolf.  "At times, the contributions of a Fellow may include enhancements to a device that immediately impacts our daily lives. At other times, new research discoveries lead to theoretical advances that, while perhaps not immediately perceptible, have substantial long-term impacts."

The 2015 ACM Fellows have been cited for contributions to key computing fields including software research, data mining, computer graphics, computer and mobile systems, system security, multiprocessor and memory architecture design, and research in sensor networks.

ACM will formally recognize the 2015 ACM Fellows at its annual Awards Banquet in June 2016 in San Francisco, California.