A machine-checked framework for relational separation logic

DOI10.1007/978-3-642-24690-6_10MaRDI QIDQ3095237zbMATH OpenOpenAlexFDO

Authors Juan Manuel Crespo, César Kunz

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

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70)

Recommendations

• Relational separation logic
• Relational logic with framing and hypotheses
• Computer Science Logic
• Beyond 2-safety: asymmetric product programs for relational program verification
• Program Verification with Separation Logic

Cites work

• scientific article; zbMATH DE number 1612488 (Why is no real title available?)
• scientific article; zbMATH DE number 1841809 (Why is no real title available?)
• A Marriage of Rely/Guarantee and Separation Logic
• A logic for information flow in object-oriented programs
• BI as an assertion language for mutable data structures
• Formal certification of code-based cryptographic proofs
• Lightweight Separation
• Practical Tactics for Separation Logic
• Programming with angelic nondeterminism
• Proving pointer programs in higher-order logic
• Proving that non-blocking algorithms don't block
• Relational separation logic
• Scalable Shape Analysis for Systems Code
• Separation Logic for Small-Step cminor
• Separation logic adapted for proofs by rewriting
• Simple relational correctness proofs for static analyses and program transformations
• Structuring the verification of heap-manipulating programs
• Types, bytes, and separation logic
• Verification of the Schorr-Waite algorithm -- from trees to graphs

Cited in

(6)

• Relational logic with framing and hypotheses
• A relation algebraic model of robust correctness
• Beyond 2-safety: asymmetric product programs for relational program verification
• scientific article; zbMATH DE number 7407781 (Why is no real title available?)
• Relational decomposition
• Relational separation logic

Describes a project that uses

Uses Software

• Coq
• VeriFast
• cminor

This page was built for publication: A machine-checked framework for relational separation logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3095237)