A concrete memory model for CompCert

DOI10.1007/978-3-319-22102-1_5MaRDI QIDQ2945624zbMATH OpenOpenAlexFDO

Authors Frédéric Besson, Sandrine Blazy, Pierre Wilke

Publication date 14 September 2015

Published in Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL https://hal.inria.fr/hal-01194549/file/paper.pdf

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20) Semantics in the theory of computing (68Q55)

Recommendations

• \textsc{CompCertS}: a memory-aware verified C compiler using a pointer as integer semantics
• CompCertS: a memory-aware verified C compiler using pointer as integer semantics
• A verified CompCert front-end for a memory model supporting pointer arithmetic and uninitialised data
• Formal verification of a C-like memory model and its uses for verifying program transformations
• A formal C memory model for separation logic

Cites work

• Aliasing restrictions of C11 formalized in Coq
• An operational and axiomatic semantics for non-determinism and sequence points in C
• Bridging the Gap: Automatic Verified Abstraction of C
• Formal verification of a C-like memory model and its uses for verifying program transformations
• Mechanized semantics for the clight subset of the C language
• Types, bytes, and separation logic

Cited in

(7)

• CompCertS: a memory-aware verified C compiler using pointer as integer semantics
• A formal C memory model for separation logic
• A verified CompCert front-end for a memory model supporting pointer arithmetic and uninitialised data
• \textsc{CompCertS}: a memory-aware verified C compiler using a pointer as integer semantics
• Concrete memory models for shape analysis
• An abstract memory functor for verified C static analyzers
• A theory of platform-dependent low-level software

This page was built for publication: A concrete memory model for CompCert

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2945624)