Qualifying CompCert for Safety-Critical Avionics Software

CompCert is the first commercially available optimizing compiler which has been formally verified. The executable code it produces is proved to behave exactly as specified by the semantics of the source C program. As a consequence, the risk of system malfunctions due to miscompilation bugs can be considered eliminated. The correctness proof of CompCert C guarantees that all safety properties verified on the source code automatically hold for the executable object code as well. In this article we will outline the qualification strategy which is used at Airbus to apply CompCert in critical avionics software in compliance to DO-178C, DO-333, and DO-330. We will describe the application context and illustrate the advantages compared to the traditional way of qualifying and certifying compilers that has been used in the past.