Sciweavers

JAR
2008

Formal Verification of a C-like Memory Model and Its Uses for Verifying Program Transformations

13 years 2 months ago
Formal Verification of a C-like Memory Model and Its Uses for Verifying Program Transformations
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.
Xavier Leroy, Sandrine Blazy
Added 13 Dec 2010
Updated 13 Dec 2010
Type Journal
Year 2008
Where JAR
Authors Xavier Leroy, Sandrine Blazy
Comments (0)