CompCertS: a memory-aware verified C compiler using pointer as integer semantics

DOI10.1007/978-3-319-66107-0_6MaRDI QIDQ1687720zbMATH OpenOpenAlexFDO

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

Publication date 4 January 2018

Full work available at URL https://hal.inria.fr/hal-01656875/file/compcerts.pdf

zbMATH Keywords

low-level codeoptimisationspointer as integerverified compilation

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20)

Recommendations

• \textsc{CompCertS}: a memory-aware verified C compiler using a pointer as integer semantics
• A concrete memory model for CompCert
• A verified CompCert front-end for a memory model supporting pointer arithmetic and uninitialised data
• Formal verification of a C-like memory model and its uses for verifying program transformations
• CompCertTSO

Cites work

• A concrete memory model for CompCert
• A formally-verified alias analysis
• Aliasing restrictions of C11 formalized in Coq
• An operational and axiomatic semantics for non-determinism and sequence points in C
• CompCertTSO

Cited in

(11)

• \textsc{CompCertS}: a memory-aware verified C compiler using a pointer as integer semantics
• CompCert
• CompCertS
• Compiling sandboxes: formally verified software fault isolation
• A formally-verified alias analysis
• Verified Compilation for Shared-Memory C
• CompCertTSO
• Automatic proofs of memory deallocation for a Whiley-to-C compiler
• An abstract memory functor for verified C static analyzers
• A concrete memory model for CompCert
• Mechanized semantics for the clight subset of the C language

Describes a project that uses

Uses Software

• CompCertTSO
• Coq

This page was built for publication: CompCertS: a memory-aware verified C compiler using pointer as integer semantics

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1687720)