Formal Verification of a C Compiler Front-end

Abstract : This paper presents the formal verification of a compiler front-end that translates a subset of the C language into the Cminor intermediate language. The semantics of the source and target languages as well as the translation between them have been written in the specification language of the Coq proof assistant. The proof of observational semantic equivalence between the source and generated code has been machine-checked using Coq. An executable compiler was obtained by automatic extraction of executable Caml code from the Coq specification of the translator, combined with a certified compiler back-end generating PowerPC assembly code from Cminor, described in previous work.
Type de document :
Communication dans un congrès
Jayadev Misra, Tobias Nipkow and Emil Sekerinski. FM'06: 14th Symposium on Formal Methods, Aug 2006, Hamilton, Canada. Springer-Verlag, 4085 (4085), pp.460-475, 2006, Lecture Notes in Computer Science; FM 2006: Formal Methods. <10.1007/11813040_31>
Liste complète des métadonnées


https://hal.inria.fr/inria-00106401
Contributeur : Sandrine Blazy <>
Soumis le : lundi 16 octobre 2006 - 10:14:34
Dernière modification le : lundi 30 juin 2008 - 13:31:16
Document(s) archivé(s) le : jeudi 20 septembre 2012 - 11:55:18

Identifiants

Collections

Citation

Sandrine Blazy, Zaynah Dargaye, Xavier Leroy. Formal Verification of a C Compiler Front-end. Jayadev Misra, Tobias Nipkow and Emil Sekerinski. FM'06: 14th Symposium on Formal Methods, Aug 2006, Hamilton, Canada. Springer-Verlag, 4085 (4085), pp.460-475, 2006, Lecture Notes in Computer Science; FM 2006: Formal Methods. <10.1007/11813040_31>. <inria-00106401>

Partager

Métriques

Consultations de
la notice

262

Téléchargements du document

156