CompCert: Practical Experience on Integrating and Qualifying a Formally Verified Optimizing Compiler

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 use of CompCert to gain certification credits for a highly safety-critical industry application, certified according to IEC 60880. We will briefly introduce the target application, illustrate the process of changing the existing compiler infrastructure to CompCert, and discuss performance characteristics. The main part focuses on the tool qualification strategy, in particular on how to take advantage of the formal correctness proof in the certification process.
Type de document :
Communication dans un congrès
ERTS2 2018 - Embedded Real Time Software and Systems, Jan 2018, Toulouse, France. 2018, 〈https://www.erts2018.org/〉
Liste complète des métadonnées

Littérature citée [25 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01643290
Contributeur : Xavier Leroy <>
Soumis le : mardi 21 novembre 2017 - 12:14:11
Dernière modification le : vendredi 1 décembre 2017 - 13:14:01

Fichier

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

Identifiants

  • HAL Id : hal-01643290, version 1

Citation

Daniel Kästner, Jörg Barrho, Ulrich Wünsche, Marc Schlickling, Bernhard Schommer, et al.. CompCert: Practical Experience on Integrating and Qualifying a Formally Verified Optimizing Compiler. ERTS2 2018 - Embedded Real Time Software and Systems, Jan 2018, Toulouse, France. 2018, 〈https://www.erts2018.org/〉. 〈hal-01643290〉

Partager

Métriques

Consultations de la notice

102

Téléchargements de fichiers

292