\textsc{CompCertS}: a memory-aware verified C compiler using a pointer as integer semantics
From MaRDI portal
Publication:2319992
DOI10.1007/s10817-018-9496-yzbMath1468.68064WikidataQ122874428 ScholiaQ122874428MaRDI QIDQ2319992
Sandrine Blazy, Pierre Wilke, Frédéric Besson
Publication date: 21 August 2019
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-018-9496-y
68N20: Theory of compilers and interpreters
Uses Software
Cites Work
- Formal verification of a C-like memory model and its uses for verifying program transformations
- A verified CompCert front-end for a memory model supporting pointer arithmetic and uninitialised data
- Aliasing Restrictions of C11 Formalized in Coq
- A Concrete Memory Model for CompCert
- A Formally-Verified Alias Analysis
- CompCertTSO
- An operational and axiomatic semantics for non-determinism and sequence points in C