|
 
|
[LB08a] Formal verification of a C-like memory model and its uses for verifying program transformations
Revue Internationale avec comité de lecture : Journal JAR, Journal of Automated Reasoning, vol. 41(1), pp. 1-31, 2008
motcle:
Résumé:
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.
BibTeX
| @article { | |||
| LB08a, | |||
| title | = | "{Formal verification of a C-like memory model and its uses for verifying program transformations}", | |
| author | = | "X. Leroy and S. Blazy", | |
| journal | = | "JAR, Journal of Automated Reasoning", | |
| year | = | 2008, | |
| volume | = | 41, | |
| number | = | 1, | |
| pages | = | "1-31", | |
| } | |||
