Formal verification of a memory model for C-like imperative languages - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2005

Formal verification of a memory model for C-like imperative languages

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.
Fichier principal
Vignette du fichier
icfem05Blazy.pdf (541.55 Ko) Télécharger le fichier
Loading...

Dates et versions

inria-00077921 , version 1 (01-06-2006)

Identifiants

Citer

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⟩
233 Consultations
205 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More