Saarbruecken, March 20, 2026 — AbsInt today officially announced
that earlier this year the formally verified
CompCert compiler was successfully qualified for the Multi-Function Computer
New Generation (MFC_NG) of ATR 42 and ATR 72 aircraft.
For the first time, certification credits for compliance with DO-178C, DO-333, and DO-330 have been successfully claimed for critical avionics software from compiler usage.
Claiming certification credits from compiler usage allows applicants to eliminate, reduce, or automate specific objectives defined by DO-178C. The use of CompCert supports the objective of verifying property preservation between source and object code — even in the presence of compiler optimizations.
As a result, test effort can be reduced. For example, formal verification performed at the source-code level can replace certain object-code testing activities otherwise required to demonstrate that the executable code complies with low-level requirements and maintains robustness.
The certification efforts and costs are further reduced by AbsInt’s accompanying Qualification Support Kit — a major advancement in the qualification of compilers for avionics software at the highest assurance levels under DO-178C.
About CompCert
CompCert is the first commercially available optimizing compiler
that has been formally verified. The machine code that it generates
is mathematically proven to exactly conform to the formal semantics
of the source C program. In recognition of its groundbreaking formal proof,
CompCert received the 2021 ACM Software System Award.
CompCert supports a wide selection of target architectures, including PowerPC, ARM, x86, RISC-V, and TriCore. It has been successfully deployed in commercial projects for many years, and previously achieved qualification for safety-critical industry applications certified under IEC 60880 and IEC 61508.
By adopting CompCert, customers improve development efficiency and benefit from significant gains in application performance, while reducing the risk of malfunctions.
For further information, visit absint.com/compcert
About AbsInt
AbsInt provides advanced development tools for embedded systems, and tools for validation, verification and certification of safety-critical and security-relevant software. As of 2026, the AbsInt product catalog includes:
- The widest selection of industry-standard tools for static analysis of binary code for a multitude of architectures;
- The most precise and comprehensive tool for static analysis of C and C++ code;
- The first and only formally verified optimizing C compiler.
Founded in 1998, AbsInt is a privately-held company located in Saarbrücken, Germany, with customers from 40+ countries and from many different industries, including aerospace, automotive, healthcare, and energy.
For further information, visit absint.com/profile.htm
Press contact:
Sylvie Tritz
+49 (681) 38 36 00
tritz[at]absint.com