A verified CompCert front-end for a memory model supporting pointer arithmetic and uninitialised data
From MaRDI portal
Publication:1739908
DOI10.1007/S10817-017-9439-ZzbMATH Open1465.68041OpenAlexW2765454105MaRDI QIDQ1739908FDOQ1739908
Authors: Frédéric Besson, Sandrine Blazy, Pierre Wilke 
Publication date: 29 April 2019
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://hal.inria.fr/hal-01656895/file/jar-besson-blazy-wilke.pdf
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 concrete memory model for CompCert
- Formal verification of a C-like memory model and its uses for verifying program transformations
- Compositional CompCert
Cites Work
- Mechanized semantics for the clight subset of the C language
- Bridging the Gap: Automatic Verified Abstraction of C
- Types, bytes, and separation logic
- A formally verified compiler back-end
- Program logics for certified compilers
- Formal verification of a C-like memory model and its uses for verifying program transformations
- Aliasing restrictions of C11 formalized in Coq
- An operational and axiomatic semantics for non-determinism and sequence points in C
- The security impact of a new cryptographic library
Cited In (5)
- \textsc{CompCertS}: a memory-aware verified C compiler using a pointer as integer semantics
- Fully Abstract and Robust Compilation
- Trace-relating compiler correctness and secure compilation
- A concrete memory model for CompCert
- CompCertS: a memory-aware verified C compiler using pointer as integer semantics
Uses Software
This page was built for publication: A verified CompCert front-end for a memory model supporting pointer arithmetic and uninitialised data
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1739908)
