Proof tactics for assertions in separation logic

DOI10.1007/978-3-319-66107-0_19MaRDI QIDQ1687747zbMATH OpenOpenAlexFDO

Authors Zhé Hóu, David Sanán, Alwen Tiu, Yang Liu

Publication date 4 January 2018

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

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Logic in computer science (03B70) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Practical Tactics for Separation Logic
• Automated theorem proving for assertions in separation logic with all connectives
• Computer Science Logic
• Charge! A framework for higher-order separation logic in Coq
• Separation logic adapted for proofs by rewriting

Cites work

• scientific article; zbMATH DE number 1948161 (Why is no real title available?)
• A Formalisation of Smallfoot in HOL
• A Marriage of Rely/Guarantee and Separation Logic
• A labelled sequent calculus for BBI: proof theory and proof search
• A theorem prover for Boolean BI
• A unified display proof theory for bunched logic
• Automated theorem proving for assertions in separation logic with all connectives
• CSimpl: a rely-guarantee-based framework for verifying concurrent programs
• Charge! A framework for higher-order separation logic in Coq
• Completeness for a first-order abstract separation logic
• Compositional shape analysis by means of bi-abduction
• Computer Science Logic
• Effective interactive proofs for higher-order imperative programs
• Expressivity Properties of Boolean BI Through Relational Models
• Higher-order separation logic in Isabelle/HOLCF
• Interactive proofs in higher-order concurrent separation logic
• Local rely-guarantee reasoning
• Mechanised Separation Algebra
• Nondeterministic phase semantics and the undecidability of Boolean BI
• On the Almighty Wand
• Parametric completeness for separation theories
• Programming Languages and Systems
• Proof search for propositional abstract separation logics via labelled sequents
• Separation logic adapted for proofs by rewriting
• The Logic of Bunched Implications
• The essence of higher-order concurrent separation logic
• Undecidability of propositional separation logic and its neighbours

Cited in

(6)

• Automated theorem proving for assertions in separation logic with all connectives
• Charge! A framework for higher-order separation logic in Coq
• Certificates and Separation Logic
• Practical Tactics for Separation Logic
• Separation logic adapted for proofs by rewriting
• Towards algebraic separation logic

Describes a project that uses

Uses Software

• CSimpl
• seL4
• Smallfoot
• Isabelle/HOL

This page was built for publication: Proof tactics for assertions in separation logic

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