A formal C memory model for separation logic

DOI10.1007/s10817-016-9369-1zbMath1386.68028arXiv1509.03339OpenAlexW2233169398WikidataQ59464114 ScholiaQ59464114MaRDI QIDQ1694027

Robbert Krebbers

Publication date: 1 February 2018

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

Full work available at URL: https://arxiv.org/abs/1509.03339

zbMATH Keywords

separation logicinteractive theorem provingCoqmemory modelsC verificationISO C11 standard

Mathematics Subject Classification ID

Uses Software

• Coq
• Flocq
• CompCertTSO
• Toolchain
• CompCert

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Formal verification of a C-like memory model and its uses for verifying program transformations
• Common Compiler Optimisations are Invalid in the C11 Memory Model and what we can do about it
• Mechanised Separation Algebra
• Aliasing Restrictions of C11 Formalized in Coq
• Verifying Object-Oriented Programs with Higher-Order Separation Logic in Coq
• Type classes for mathematics in type theory
• Types, bytes, and separation logic
• Separation Logic for Non-local Control Flow and Block Scope Variables
• A Formally-Verified Alias Analysis
• An Intrinsic Encoding of a Subset of C and its Application to TLS Network Packet Processing
• A Formalization of the C99 Standard in HOL, Isabelle and Coq
• Permission accounting in separation logic
• CONCUR 2004 - Concurrency Theory
• Handcrafted Inversions Made Operational on Operational Semantics
• Formal certification of a compiler back-end or
• CompCertTSO
• 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
• Verified Compilation for Shared-Memory C
• Oracle Semantics for Concurrent Separation Logic
• Program Logics for Certified Compilers

This page was built for publication: A formal C memory model for separation logic