CompCert development team receives this year’s ACM Software System Award

These leaders were selected by their peers for making contributions to groundbreaking research and practical applications that impact people using technology every day.

The ACM Software System Award is presented to an institution or individual(s) recognized for developing a software system that has had a lasting influence, reflected in contributions to concepts, in commercial acceptance, or both. In the past, the price has been awarded e.g. for the development of the UNIX operating system and the World Wide Web.

This year’s Award goes to the developers of CompCert, the first practically useful optimizing compiler targeting multiple commercial architectures that has a complete, mechanically checked proof of its correctness.

The recipients of the Award are:

• 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 GmbH;
• Bernhard Schommer, Saarland University and AbsInt Angewandte Informatik GmbH;
• Jean-Baptiste Tristan, Boston College.

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. Other researchers build on CompCert, and multiple corporations use it in the development of their safety-critical applications. AbsInt offers commercial licenses, provides industrial-strength technical support and maintenance, and actively contributes to further advancement of the tool.

About ACM

ACM, the Association for Computing Machinery, is the world’s largest educational and scientific computing society, uniting computing educators, researchers and professionals to inspire dialogue, share resources and address the field’s challenges. ACM strengthens the computing profession’s collective voice through strong leadership, promotion of the highest standards, and recognition of technical excellence. ACM supports the professional growth of its members by providing opportunities for life-long learning, career development, and professional networking.

For further information, visit www.acm.org.