Closing the Gap – The Formally Verified Optimizing Compiler CompCert

Daniel Kästner 1 Xavier Leroy 2 Sandrine Blazy 3 Bernhard Schommer 1 Michael Schmidt 1 Christian Ferdinand 1
1 Angewandte Informatik - AbsInt GmbH
2 GALLIUM - Programming languages, types, compilation and proofs
Inria Paris-Rocquencourt
3 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA_D4 - LANGAGE ET GÉNIE LOGICIEL
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.
Type de document :
Communication dans un congrès
SSS'17: Safety-critical Systems Symposium 2017, Feb 2017, Bristol, United Kingdom. CreateSpace, pp.163-180, 2017, Developments in System Safety Engineering: Proceedings of the Twenty-fifth Safety-critical Systems Symposium
Liste complète des métadonnées

Littérature citée [8 références]  Voir  Masquer  Télécharger
https://hal.inria.fr/hal-01399482
Contributeur : Xavier Leroy <>
Soumis le : vendredi 18 novembre 2016 - 21:36:56
Dernière modification le : jeudi 15 novembre 2018 - 11:58:59
Document(s) archivé(s) le : mardi 21 mars 2017 - 07:30:24

Fichier

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

Identifiants

  • HAL Id : hal-01399482, version 1

Collections

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

Citation

Daniel Kästner, Xavier Leroy, Sandrine Blazy, Bernhard Schommer, Michael Schmidt, et al.. Closing the Gap – The Formally Verified Optimizing Compiler CompCert. SSS'17: Safety-critical Systems Symposium 2017, Feb 2017, Bristol, United Kingdom. CreateSpace, pp.163-180, 2017, Developments in System Safety Engineering: Proceedings of the Twenty-fifth Safety-critical Systems Symposium. 〈hal-01399482〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

3979

Téléchargements de fichiers

14329

Contact


archive-ouverte@inria.fr