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

DOI10.1007/978-3-319-66107-0_6zbMath1468.68063OpenAlexW2746152268MaRDI QIDQ1687720

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

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)

Related Items (2)

CompCert ⋮ CompCertS

Uses Software

• Coq
• CompCertTSO

Cites Work

• 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

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