CompCert Qualification Achieved for Avionics Software
AbsInt is proud to announce that at the beginning of 2026 the CompCert compiler has officially been qualified for the Multi-Function Computer New Generation (MFC_NG) of ATR 42/72 aircrafts. For the first time, certification credits from compiler usage can be claimed for critical avionics software in compliance with DO-178C, DO-333, and DO-330.
Successful qualification of CompCert for the Multi-Function Computer New Generation (MFC_NG) of ATR 42/72 aircrafts
Claiming certification credits from a compiler 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 AbsInt Qualification Support Kit further reduces certification effort and cost. It represents a major advancement in the qualification of compilers for avionics software at the highest assurance levels under DO-178C.
CompCert is the first commercially available optimizing compiler to be formally verified. The machine code it generates is mathematically proven to conform exactly to the formal semantics of the source C program. CompCert supports multiple target architectures, including PowerPC, ARM, TriCore, RISC-V, and x86.
In recognition of its groundbreaking formal proof, CompCert received the ACM Software System Award in 2021. It has been successfully deployed in commercial projects for many years and has also been qualified in safety-critical industry applications certified under IEC 60880.
By adopting CompCert, organizations can achieve significant gains in application performance and development efficiency while reducing the risk of malfunctions due to miscompilation.
If you have any questions, please do not hesitate to contact us.
RELATED NEWS
From Perpetual Licensing to UBL
Perpetual licenses have been a trusted option for embedded development for many years. However, as development environments become more connected and automated, Arm's User-Based Licensing (UBL) o[...]
Read more
ARCHITECTURE OF TRUST: STRENGTHENING SECURITY IN MODERN CORTEX-M SYSTEMS
As embedded devices continue to expand into connected and safety-critical applications, security has become a fundamental design requirement rather than an optional feature. From industrial contr[...]
Read more
CompCert: Advancing Confidence in Safety-Critical Software Development
In the modern age where everything is run by software, the reliability of software toolchains plays a crucial role in safety critical industries such as aerospace, automotive and industrial appli[...]
Read more
Safe and Efficient AUTOSAR Development with ISO 26262 Verification
AUTOSAR defines how software is structured. QA Systems tools prove that the software is safe. AUTOSAR provides a standardised software architecture that underpins much of today’s automotive ECU [...]
Read more
Embedded Debugging Tools: How Atlas Hardware Models with Arm DS IDE
If you’ve ever tried to validate embedded behavior in a virtual environment, you know the pain: you can observe what the system does, but the moment you need to interact with it—drive a pin hi[...]
Read more
PRODUCTS
Manufacturers
Resource center