|
 
|
[BL05] Formal verification of a memory model for C-like imperative languages
Conférence Internationale avec comité de lecture : ICFEM'05, Int. Conf on Formal Engineering Methods, Manchester, UK, January 2005, Vol. 3785, pp.280-299, Series LNCS,
motcle:
Résumé:
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.
BibTeX
| @inproceedings { | |||
| BL05, | |||
| title | = | "{Formal verification of a memory model for C-like imperative languages}", | |
| author | = | " S. Blazy and X. Leroy ", | |
| booktitle | = | "{ICFEM'05, Int. Conf on Formal Engineering Methods, Manchester, UK}", | |
| year | = | 2005, | |
| month | = | "January", | |
| series | = | "LNCS", | |
| volume | = | 3785, | |
| pages | = | "280-299", | |
| } | |||
