A Concrete Memory Model for CompCert

DOI10.1007/978-3-319-22102-1_5zbMath1465.68040OpenAlexW1526037585MaRDI QIDQ2945624

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

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)

Related Items (2)

CompCertS: a memory-aware verified C compiler using pointer as integer semantics ⋮ \textsc{CompCertS}: a memory-aware verified C compiler using a pointer as integer semantics

Cites Work

• 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
• Bridging the Gap: Automatic Verified Abstraction of C
• Aliasing Restrictions of C11 Formalized in Coq
• Types, bytes, and separation logic
• An operational and axiomatic semantics for non-determinism and sequence points in C

This page was built for publication: A Concrete Memory Model for CompCert