A verified CompCert front-end for a memory model supporting pointer arithmetic and uninitialised data

DOI10.1007/s10817-017-9439-zzbMath1465.68041OpenAlexW2765454105MaRDI QIDQ1739908

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

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

zbMATH Keywords

verified compilationC semanticspointer arithmetic

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20) Semantics in the theory of computing (68Q55)

Related Items (2)

Trace-Relating Compiler Correctness and Secure Compilation ⋮ \textsc{CompCertS}: a memory-aware verified C compiler using a pointer as integer semantics

Uses Software

• z3
• VCC
• CVC4
• Toolchain
• CompCert
• NaCl
• Verasco

Cites Work

• 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
• A formally verified compiler back-end
• Bridging the Gap: Automatic Verified Abstraction of C
• The Security Impact of a New Cryptographic Library
• Aliasing Restrictions of C11 Formalized in Coq
• Types, bytes, and separation logic
• An operational and axiomatic semantics for non-determinism and sequence points in C
• Program Logics for Certified Compilers

This page was built for publication: A verified CompCert front-end for a memory model supporting pointer arithmetic and uninitialised data