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
Configuring QA-MISRA for Real-World Embedded C/C++ Projects
Once QA-MISRA has been set up for a C or C++ project, the next step is adapting the analysis to the requirements of the development team. Different projects may follow different coding standard[...]
Read more
Setting Up a QA-MISRA Evaluation License and VS Code Extension
The following steps explain how to activate a QA-MISRA evaluation license, configure the local server, install the QA-MISRA extension in Visual Studio Code, and run an example analysis. 1. Requ[...]
Read more
Using QA-MISRA to Bring Coding Standards into C/C++ Development
In embedded and safety-critical software, coding standards help reduce risky language behaviour, improve consistency, and make software easier to review and verify. This is especially important i[...]
Read more
When Breakpoints Aren’t Enough: Debugging Faster with ULINKpro Trace
Most embedded developers are familiar with the usual debugging cycle: set a breakpoint, stop the processor, inspect the problem, make a change, and try again. That works well until the problem [...]
Read more
How Static Analysis Supports DO-178C Verification
Developing software for airborne systems requires strong verification evidence, especially for higher-criticality applications. DO-178C defines objectives for airborne software development and ve[...]
Read more
EMBEDDED IS EVERYWHERE
PRODUCTS
Manufacturers
Resource center