Formal verification of a memory model for C-like imperative languages

Sandrine Blazy 1, 2, 3 Xavier Leroy 1, 2
1 INRIA Rocquencourt
2 CRISTAL - Typed programming, modularity and compilation
Inria Paris-Rocquencourt
3 CEDRIC - Centre d'Etude et De Recherche en Informatique du Cnam
Abstract : This paper presents a formal verification with the Coq proof assistant of a memory model for C-like imperative languages. This model defines the memory layout and the operations that manage the memory. The model has been specified at two levels of abstraction and implemented as part of an ongoing certification in Coq of a moderately-optimising C compiler. Many properties of the memory have been verified in the specification. They facilitate the definition of precise formal semantics of C pointers. A certified OCaml code implementing the memory model has been automatically extracted from the specifications.
Type de document :
Communication dans un congrès
Kung-Kiu Lau, Richard Banach. ICFEM'05: 7th International Conference on Formal Engineering Methods, Nov 2005, Manchester, United Kingdom. Springer, 3785 (3785), pp.280-299, 2005, Lecture Notes in Computer Science. 〈10.1007/11576280〉
Liste complète des métadonnées

Littérature citée [25 références]  Voir  Masquer  Télécharger
https://hal.inria.fr/inria-00077921
Contributeur : Sandrine Blazy <>
Soumis le : jeudi 1 juin 2006 - 16:03:35
Dernière modification le : dimanche 1 avril 2018 - 10:28:02
Document(s) archivé(s) le : mardi 18 septembre 2012 - 14:30:19

Fichier

icfem05Blazy.pdf

Identifiants

Collections

INRIA

Citation

Sandrine Blazy, Xavier Leroy. Formal verification of a memory model for C-like imperative languages. Kung-Kiu Lau, Richard Banach. ICFEM'05: 7th International Conference on Formal Engineering Methods, Nov 2005, Manchester, United Kingdom. Springer, 3785 (3785), pp.280-299, 2005, Lecture Notes in Computer Science. 〈10.1007/11576280〉. 〈inria-00077921〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

303

Téléchargements de fichiers

121

Contact


archive-ouverte@inria.fr