\textsc{CompCertS}: a memory-aware verified C compiler using a pointer as integer semantics
From MaRDI portal
Publication:2319992
Recommendations
- 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
- CompCertTSO
- Exploiting pointer analysis in memory models for deductive verification
- An abstract memory functor for verified C static analyzers
- Compositional verification of compiler optimisations on relaxed memory
Cites work
- A concrete memory model for CompCert
- A formally-verified alias analysis
- A verified CompCert front-end for a memory model supporting pointer arithmetic and uninitialised data
- Aliasing restrictions of C11 formalized in Coq
- An operational and axiomatic semantics for non-determinism and sequence points in C
- CompCertTSO
- Formal verification of a C-like memory model and its uses for verifying program transformations
Cited in
(9)- 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
- Automatic proofs of memory deallocation for a Whiley-to-C compiler
- Mechanized semantics for the clight subset of the C language
- A concrete memory model for CompCert
- An abstract memory functor for verified C static analyzers
- A formally-verified alias analysis
- Compiling sandboxes: formally verified software fault isolation
- Defining and preserving more C behaviors: verified compilation using a concrete memory model
This page was built for publication: \textsc{CompCertS}: a memory-aware verified C compiler using a pointer as integer semantics
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2319992)
