Formal verification of a C-like memory model and its uses for verifying program transformations

Abstract : This article presents the formal verification, using the Coq proof assistant, of a memory model for low-level imperative languages such as C and compiler intermediate languages. Beyond giving semantics to pointer-based programs, this model supports reasoning over transformations of such programs. We show how the properties of the memory model are used to prove semantic preservation for three passes of the Compcert verified compiler
Type de document :
Article dans une revue
Journal of Automated Reasoning, Springer Verlag, 2008, 41 (1), pp.1-31. 〈10.1007/s10817-008-9099-0〉
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00289542
Contributeur : Xavier Leroy <>
Soumis le : samedi 21 juin 2008 - 13:21:52
Dernière modification le : lundi 5 octobre 2015 - 16:58:39
Document(s) archivé(s) le : vendredi 28 septembre 2012 - 16:25:45

Fichier

memory-model-journal.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Xavier Leroy, Sandrine Blazy. Formal verification of a C-like memory model and its uses for verifying program transformations. Journal of Automated Reasoning, Springer Verlag, 2008, 41 (1), pp.1-31. 〈10.1007/s10817-008-9099-0〉. 〈inria-00289542〉

Partager

Métriques

Consultations de
la notice

255

Téléchargements du document

155