Proof tactics for assertions in separation logic

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

Mathematics Subject Classification ID

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

• Isabelle/HOL
• Smallfoot
• seL4
• CSimpl

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