A formally verified compiler back-end

Xavier Leroy 1, 2, *
Abstract : This article describes the development and formal verification (proof of semantic preservation) of a compiler back-end from Cminor (a simple imperative intermediate language) to PowerPC assembly code, using the Coq proof assistant both for programming the compiler and for proving its correctness. Such a verified compiler is useful in the context of formal methods applied to the certification of critical software: the verification of the compiler guarantees that the safety properties proved on the source code hold for the executable compiled code as well.
Type de document :
Article dans une revue
Journal of Automated Reasoning, Springer Verlag, 2009, 43 (4), pp.363-446. <10.1007/s10817-009-9155-4>
Liste complète des métadonnées


https://hal.inria.fr/inria-00360768
Contributeur : Xavier Leroy <>
Soumis le : samedi 14 novembre 2009 - 09:50:59
Dernière modification le : lundi 5 octobre 2015 - 17:00:31
Document(s) archivé(s) le : jeudi 23 septembre 2010 - 17:45:04

Fichiers

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

Identifiants

Collections

Citation

Xavier Leroy. A formally verified compiler back-end. Journal of Automated Reasoning, Springer Verlag, 2009, 43 (4), pp.363-446. <10.1007/s10817-009-9155-4>. <inria-00360768v3>

Partager

Métriques

Consultations de
la notice

385

Téléchargements du document

270