A verified CompCert front-end for a memory model supporting pointer arithmetic and uninitialised data
From MaRDI portal
(Redirected from Publication:1739908)
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
- A formally verified compiler back-end
- 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
- Program logics for certified compilers
- The security impact of a new cryptographic library
- Types, bytes, and separation logic
Cited in
(5)- CompCertS: a memory-aware verified C compiler using pointer as integer semantics
- Fully Abstract and Robust Compilation
- \textsc{CompCertS}: a memory-aware verified C compiler using a pointer as integer semantics
- A concrete memory model for CompCert
- Trace-relating compiler correctness and secure compilation
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)
