A machine-checked framework for relational separation logic
DOI10.1007/978-3-642-24690-6_10zbMATH Open1350.68059OpenAlexW2121753233MaRDI QIDQ3095237FDOQ3095237
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
Recommendations
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)
Cites Work
- Separation Logic for Small-Step cminor
- Formal certification of code-based cryptographic proofs
- BI as an assertion language for mutable data structures
- Title not available (Why is that?)
- Scalable Shape Analysis for Systems Code
- Proving that non-blocking algorithms don't block
- A Marriage of Rely/Guarantee and Separation Logic
- Programming with angelic nondeterminism
- Proving pointer programs in higher-order logic
- Types, bytes, and separation logic
- Title not available (Why is that?)
- Relational separation logic
- A logic for information flow in object-oriented programs
- Simple relational correctness proofs for static analyses and program transformations
- Verification of the Schorr-Waite Algorithm – From Trees to Graphs
- Lightweight Separation
- Structuring the verification of heap-manipulating programs
- Separation Logic Adapted for Proofs by Rewriting
- Practical Tactics for Separation Logic
Cited In (2)
Uses Software
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)
