Automated Theorem Proving for Assertions in Separation Logic with All Connectives

DOI10.1007/978-3-319-21401-6_34zbMath1465.03053OpenAlexW1448383169MaRDI QIDQ3454118

Zhé Hóu, Rajeev Goré, Alwen Tiu

Publication date: 2 December 2015

Published in: Automated Deduction - CADE-25 (Search for Journal in Brave)

Full work available at URL: http://hdl.handle.net/10072/395146

Mathematics Subject Classification ID

Logic in computer science (03B70) Mechanization of proofs and logical operations (03B35) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (6)

Expressive Completeness of Separation Logic with Two Variables and No Separating Conjunction ⋮ Completeness for a First-Order Abstract Separation Logic ⋮ Proof tactics for assertions in separation logic ⋮ On Temporal and Separation Logics ⋮ A Complete Decision Procedure for Linearly Compositional Separation Logic with Data Constraints ⋮ Unnamed Item

Uses Software

• VeriStar
• Smallfoot
• jStar

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• On the almighty wand
• A semantics for concurrent separation logic
• A Labelled Sequent Calculus for BBI: Proof Theory and Proof Search
• Fictional Separation Logic
• The ramifications of sharing in data structures
• Separation Logic Modulo Theories
• Tableaux and Resource Graphs for Separation Logic
• A Marriage of Rely/Guarantee and Separation Logic
• Modular Safety Checking for Fine-Grained Concurrency
• Separation Logic for Higher-Order Store
• The Logic of Bunched Implications
• Expressive completeness of separation logic with two variables and no separating conjunction
• Separation Logic with One Quantified Variable
• Verified heap theorem prover by paramodulation
• Automated Cyclic Entailment Proofs in Separation Logic
• Proof search for propositional abstract separation logics via labelled sequents
• A proof system for separation logic with magic wand
• Programming Languages and Systems
• Proof automation for functional correctness in separation logic

This page was built for publication: Automated Theorem Proving for Assertions in Separation Logic with All Connectives