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 applications. Traditional compilers are, although highly capable, can occasionally introduce miscompilation issues that may impact system behaviour in unexpected ways.
This brings us to CompCert, which is the world's first commercially available formally verified optimizing C compiler, and is being qualified for its use in highly critical avionics applications at Airbus. Unlike conventional compilers that primarily rely on extensive testing, CompCert uses mathematical proofs to demonstrate semantic preservation, ensuring generated executable code behaves consistently with the original source code.
By reducing the risks associated with compiler errors and while still maintaining optimization capabilities, this approach can help improve confidence and efficiency in software development workflows, reducing the time in verification in safety critical applications.
As safety requirements continue to evolve, technologies like CompCert, which are backed by mathematical proof rather than testing alone, represent an important step toward building more reliable embedded systems.
If you would like to evaluate CompCert or need any further information, please feel free to reach out to Robert Campbell at Robert.Campbell@joraltechnologies.com
Qualifying CompCert for Safety-Critical Avionics Software - Click here to review the full article.
RELATED NEWS
Beyond Code Generation: AI-Assisted Embedded Development with Arm CMSIS
AI coding assistants can generate a UART driver in seconds. But when the output is garbled or an application unexpectedly enters a HardFault handler, the problem may not be obvious from the sourc[...]
Read more
Configuring QA-MISRA for Real-World Embedded C/C++ Projects
Getting QA-MISRA running is only the first part of the setup. For an actual embedded project, you will usually need to decide which coding rules should be checked, how compiler-specific code sho[...]
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
EMBEDDED IS EVERYWHERE
PRODUCTS
Manufacturers
Resource center