New York, NY, May 11, 2022 — ACM, the Association for Computing Machinery, today announced the recipients of the prestigious 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. The Software System Award carries a prize of $35,000. Financial support for the Award is provided by IBM.
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.
First devised in 2005, CompCert remains to this day the only industrial-strength C 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-bit).
Thanks to having been formally verified using machine-assisted mathematical proofs, CompCert represents a major advance over other production compilers, because it does not experience any miscompilation issues. Code produced by CompCert is guaranteed to behave exactly as specified by the semantics of the source C program.
This level of confidence in the correctness of the compilation process is second to none and thus enables CompCert users to meet the highest levels of software assurance no other compiler can support.
To this day, CompCert continues as a research project at Inria, the French National Institute for Research in Digital Science and Technology. Other research groups from all around the world build on CompCert, and numerous corporations from various market segments 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 AbsInt
AbsInt provides cutting-edge development tools for embedded systems with a focus on validation, verification, and certification of safety-critical and security-relevant software. Key products include static analysis tools to check coding guidelines, for timing and stack usage analysis, and to detect critical programming defects in C/C++ code, as well as the formally verified CompCert Compiler.
Founded in 1998, AbsInt is a privately-held company located in Saarbrücken, Germany. Its customers come from various industry sectors, including aerospace, automotive, healthcare and energy, and are located in more than 40 countries all over the world.
For further information, visit absint.com.
Press contact:
Sylvie Tritz
+49 (681) 38 36 00
tritz[at]absint.com
This press release is available for download as PDF in English and German.