CompCert – A Formally Verified Optimizing Compiler

CompCert is the first commercially available optimiz-ing compiler that is formally verified, using machine-assisted mathematical proofs, to be exempt from mis-compilation. The executable code it produces is proved to behave exactly as specified by the semantics of the source C program. This article gives an overview of the design of CompCert and its proof concept and then focuses on aspects relevant for industrial application. We briefly summarize practical experience and give an overview of recent CompCert development aiming at in-dustrial usage. CompCert’s intended use is the compi-lation of life-critical and mission-critical software meet-ing high levels of assurance. In this context tool quali-fication is of paramount importance. We summarize the confidence argument of CompCert and give an overview of relevant qualification strategies. 1