Proof tactics for assertions in separation logic
From MaRDI portal
Publication:1687747
DOI10.1007/978-3-319-66107-0_19zbMath1483.03004OpenAlexW2749928091MaRDI QIDQ1687747
David Sanán, Zhé Hóu, Yang Liu, Alwen Tiu
Publication date: 4 January 2018
Full work available at URL: http://hdl.handle.net/10072/395142
Logic in computer science (03B70) Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Uses Software
Cites Work
- Unnamed Item
- A Labelled Sequent Calculus for BBI: Proof Theory and Proof Search
- Charge!
- Mechanised Separation Algebra
- A theorem prover for Boolean BI
- Effective interactive proofs for higher-order imperative programs
- Nondeterministic Phase Semantics and the Undecidability of Boolean BI
- The Essence of Higher-Order Concurrent Separation Logic
- A Unified Display Proof Theory for Bunched Logic
- Completeness for a First-Order Abstract Separation Logic
- A Formalisation of Smallfoot in HOL
- Undecidability of Propositional Separation Logic and Its Neighbours
- CSimpl: A Rely-Guarantee-Based Framework for Verifying Concurrent Programs
- Automated Theorem Proving for Assertions in Separation Logic with All Connectives
- A Marriage of Rely/Guarantee and Separation Logic
- On the Almighty Wand
- The Logic of Bunched Implications
- Local rely-guarantee reasoning
- Interactive proofs in higher-order concurrent separation logic
- Expressivity Properties of Boolean BI Through Relational Models
- Computer Science Logic
- Compositional Shape Analysis by Means of Bi-Abduction
- Parametric completeness for separation theories
- Proof search for propositional abstract separation logics via labelled sequents
- Higher-Order Separation Logic in Isabelle/HOLCF
- Programming Languages and Systems
- Separation Logic Adapted for Proofs by Rewriting
