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'études et de recherche en informatique et communications
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.
Document type :
Conference papers
Complete list of metadatas

Cited literature [25 references]  Display  Hide  Download
https://hal.inria.fr/inria-00077921
Contributor : Sandrine Blazy <>
Submitted on : Thursday, June 1, 2006 - 4:03:35 PM
Last modification on : Saturday, February 9, 2019 - 1:23:01 AM
Long-term archiving on : Tuesday, September 18, 2012 - 2:30:19 PM

File

icfem05Blazy.pdf

Identifiers

Collections

INRIA | INRIA-ROCQ

Citation

Sandrine Blazy, Xavier Leroy. Formal verification of a memory model for C-like imperative languages. ICFEM'05: 7th International Conference on Formal Engineering Methods, Nov 2005, Manchester, United Kingdom. pp.280-299, ⟨10.1007/11576280⟩. ⟨inria-00077921⟩

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

392

Files downloads

262

Contact


archive-ouverte@inria.fr