A Machine-Checked Framework for Relational Separation Logic

DOI10.1007/978-3-642-24690-6_10zbMath1350.68059MaRDI QIDQ3095237

César Kunz, Juan Manuel Crespo

Publication date: 28 October 2011

Published in: Software Engineering and Formal Methods (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-24690-6_10

Mathematics Subject Classification ID

03B70: Logic in computer science

68Q60: Specification and verification (program logics, model checking, etc.)

68N30: Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)

Uses Software

• Coq
• VeriFast
• cminor

Cites Work

• Unnamed Item
• Unnamed Item
• Relational separation logic
• Proving pointer programs in higher-order logic
• Verification of the Schorr-Waite Algorithm – From Trees to Graphs
• Practical Tactics for Separation Logic
• Types, bytes, and separation logic
• Simple relational correctness proofs for static analyses and program transformations
• Scalable Shape Analysis for Systems Code
• Separation Logic for Small-Step cminor
• A Marriage of Rely/Guarantee and Separation Logic
• Lightweight Separation
• BI as an assertion language for mutable data structures
• Structuring the verification of heap-manipulating programs
• Programming with angelic nondeterminism
• Proving that non-blocking algorithms don't block
• Formal certification of code-based cryptographic proofs
• A logic for information flow in object-oriented programs
• Separation Logic Adapted for Proofs by Rewriting