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

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 : lundi 30 juin 2008 - 13:29:58
Document(s) archivé(s) le : mardi 18 septembre 2012 - 14:30:19

Identifiants

Collections

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〉

Partager

Métriques

Consultations de
la notice

281

Téléchargements du document

104