Formal verification of a C-like memory model and its uses for verifying program transformations

DOI10.1007/s10817-008-9099-0zbMath1154.68039OpenAlexW2154942048MaRDI QIDQ945054

Sandrine Blazy, Xavier Leroy

Publication date: 10 September 2008

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://hal.inria.fr/inria-00289542/file/memory-model-journal.pdf

zbMATH Keywords

compilationmemory modelprogram verificationCoq proof assistantcompiler correctnessC

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

Formal verification of C systems code. Structured types, separation logic and theorem proving, Beyond 2-Safety: Asymmetric Product Programs for Relational Program Verification, Certified verification of relational properties, Mechanized semantics for the clight subset of the C language, A formally verified compiler back-end, Toward compositional verification of interruptible OS kernels and device drivers, Mechanising a type-safe model of multithreaded Java with a verified compiler, Aliasing Restrictions of C11 Formalized in Coq, A Concrete Memory Model for CompCert, A formal C memory model for separation logic, Verified Software Toolchain, A verified CompCert front-end for a memory model supporting pointer arithmetic and uninitialised data, JNI light: an operational model for the core JNI, Memory Policy Analysis for Semantics Specifications in Maude, \textsc{CompCertS}: a memory-aware verified C compiler using a pointer as integer semantics

Uses Software

• Coq
• z3
• SIMPLIFY
• cminor
• UMM

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Abstract models of storage
• Proving pointer programs in higher-order logic
• Types, bytes, and separation logic
• A theory of platform-dependent low-level software
• Separation Logic for Small-Step cminor
• Simplify: a theorem prover for program checking
• The Java memory model
• Formal certification of a compiler back-end or
• Programming Languages and Systems