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.

Visit the CompCert Product Page