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
Document type :
Journal articles
Complete list of metadatas

Cited literature [26 references]  Display  Hide  Download

https://hal.inria.fr/inria-00289542
Contributor : Xavier Leroy <>
Submitted on : Saturday, June 21, 2008 - 1:21:52 PM
Last modification on : Saturday, February 9, 2019 - 1:23:16 AM
Long-term archiving on : Friday, September 28, 2012 - 4:25:45 PM

File

memory-model-journal.pdf
Files produced by the author(s)

Identifiers

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⟩

Share

Metrics

Record views

449

Files downloads

372