Aliasing Restrictions of C11 Formalized in Coq

DOI10.1007/978-3-319-03545-1_4zbMath1426.68055OpenAlexW201976661MaRDI QIDQ2938039

Robbert Krebbers

Publication date: 13 January 2015

Published in: Certified Programs and Proofs (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-03545-1_4

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Formalization of mathematics in connection with theorem provers (68V20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (6)

A Concrete Memory Model for CompCert ⋮ CompCertS: a memory-aware verified C compiler using pointer as integer semantics ⋮ A formal C memory model for separation logic ⋮ A verified CompCert front-end for a memory model supporting pointer arithmetic and uninitialised data ⋮ Typing with Leftovers - A mechanization of Intuitionistic Multiplicative-Additive Linear Logic ⋮ \textsc{CompCertS}: a memory-aware verified C compiler using a pointer as integer semantics

Uses Software

• Coq
• Isabelle
• HOL
• CompCert

Cites Work

• Formal verification of a C-like memory model and its uses for verifying program transformations
• Types, bytes, and separation logic
• A theory of platform-dependent low-level software
• Separation Logic for Non-local Control Flow and Block Scope Variables
• A Formally-Verified Alias Analysis
• A Formalization of the C99 Standard in HOL, Isabelle and Coq
• An operational and axiomatic semantics for non-determinism and sequence points in C
• Mathematizing C++ concurrency
• Formal verification of object layout for c++ multiple inheritance

This page was built for publication: Aliasing Restrictions of C11 Formalized in Coq