CompCert - A Formally Verified Optimizing Compiler

Xavier Leroy 1 Sandrine Blazy 2 Daniel Kästner 3 Bernhard Schommer 3 Markus Pister 3 Christian Ferdinand 3
1 GALLIUM - Langages de programmation, types, compilation et preuves
Inria de Paris
2 CELTIQUE - Software certification with semantic analysis
IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL, Inria Rennes – Bretagne Atlantique
3 Angewandte Informatik - AbsInt GmbH
Abstract : CompCert is the first commercially available optimizing 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 industrial usage. CompCert's intended use is the compilation of life-critical and mission-critical software meeting high levels of assurance. In this context tool qualification is of paramount importance. We summarize the confidence argument of CompCert and give an overview of relevant qualification strategies.
Type de document :
Communication dans un congrès
ERTS 2016: Embedded Real Time Software and Systems, 8th European Congress, Jan 2016, Toulouse, France. 〈http://www.erts2016.org/〉
Liste complète des métadonnées

Littérature citée [12 références]  Voir  Masquer  Télécharger
https://hal.inria.fr/hal-01238879
Contributeur : Xavier Leroy <>
Soumis le : lundi 7 décembre 2015 - 11:39:54
Dernière modification le : mercredi 16 mai 2018 - 11:23:28
Document(s) archivé(s) le : samedi 29 avril 2017 - 05:26:15

Fichier

erts2016_compcert.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01238879, version 1

Collections

INRIA | IRISA | ERTS2016 | UR1-UFR-ISTIC | CENTRALESUPELEC | UNIV-RENNES | INRIA-ROCQ

Citation

Xavier Leroy, Sandrine Blazy, Daniel Kästner, Bernhard Schommer, Markus Pister, et al.. CompCert - A Formally Verified Optimizing Compiler. ERTS 2016: Embedded Real Time Software and Systems, 8th European Congress, Jan 2016, Toulouse, France. 〈http://www.erts2016.org/〉. 〈hal-01238879〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

1114

Téléchargements de fichiers

370

Contact


archive-ouverte@inria.fr