| HAL-Inria | Publications, software ... of Inria's scientists |
Conference papers
Closing the Gap – The Formally Verified Optimizing Compiler CompCert
Abstract : CompCert is the first commercially available optimizing compiler that is formally verified, using machine-assisted mathematical proofs, to be free from miscompilation. The executable code it produces is proved to behave exactly as specified by the semantics of the source C program. CompCert's intended use is the compilation of safety-critical and mission-critical software meeting high levels of assurance. This article gives an overview of the design of CompCert and its proof concept, summarizes the resulting confidence argument, and gives an overview of relevant tool qualification strategies. We briefly summarize practical experience and give an overview of recent CompCert developments.
Cited literature [8 references]
https://hal.inria.fr/hal-01399482
Contributor : Xavier Leroy <>
Submitted on : Friday, November 18, 2016 - 9:36:56 PM
Last modification on : Saturday, November 21, 2020 - 7:58:02 PM
Long-term archiving on: : Tuesday, March 21, 2017 - 7:30:24 AM
Contributor : Xavier Leroy <>
Submitted on : Friday, November 18, 2016 - 9:36:56 PM
Last modification on : Saturday, November 21, 2020 - 7:58:02 PM
Long-term archiving on: : Tuesday, March 21, 2017 - 7:30:24 AM
File
SSS2017_kaestner_et_al.pdf
Files produced by the author(s)