Completeness for a first-order abstract separation logic

DOI10.1007/978-3-319-47958-3_23MaRDI QIDQ3179309zbMATH OpenOpenAlexFDO

Authors Zhé Hóu, Alwen Tiu

Publication date 21 December 2016

Published in Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1608.06729

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)

Abstract: Existing work on theorem proving for the assertion language of separation logic (SL) either focuses on abstract semantics which are not readily available in most applications of program verification, or on concrete models for which completeness is not possible. An important element in concrete SL is the points-to predicate which denotes a singleton heap. SL with the points-to predicate has been shown to be non-recursively enumerable. In this paper, we develop a first-order SL, called FOASL, with an abstracted version of the points-to predicate. We prove that FOASL is sound and complete with respect to an abstract semantics, of which the standard SL semantics is an instance. We also show that some reasoning principles involving the points-to predicate can be approximated as FOASL theories, thus allowing our logic to be used for reasoning about concrete program verification problems. We give some example theories that are sound with respect to different variants of separation logics from the literature, including those that are incompatible with Reynolds's semantics. In the experiment we demonstrate our FOASL based theorem prover which is able to handle a large fragment of separation logic with heap semantics as well as non-standard semantics.

Recommendations

• Completeness and expressiveness of pointer program verification by separation logic
• Automated theorem proving for assertions in separation logic with all connectives
• Computer Science Logic
• Proof search for propositional abstract separation logics via labelled sequents
• Expressive completeness of separation logic with two variables and no separating conjunction

Cites work

• A Marriage of Rely/Guarantee and Separation Logic
• A proof system for separation logic with magic wand
• A semantics for concurrent separation logic
• A theorem prover for Boolean BI
• A unified display proof theory for bunched logic
• Automated cyclic entailment proofs in separation logic
• Automated theorem proving for assertions in separation logic with all connectives
• Completeness for a first-order abstract separation logic
• Exploring the relation between Intuitionistic BI and Boolean BI: an unexpected embedding
• Expressive completeness of separation logic with two variables and no separating conjunction
• Fictional separation logic
• scientific article; zbMATH DE number 2081098 (Why is no real title available?)
• scientific article; zbMATH DE number 949290 (Why is no real title available?)
• scientific article; zbMATH DE number 1841809 (Why is no real title available?)
• Looking at separation algebras with Boolean BI-eyes
• 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 with one quantified variable
• Tableaux and resource graphs for separation logic
• The formal strong completeness of partial monoidal Boolean BI
• The Logic of Bunched Implications
• The semantics of BI and resource tableaux
• Undecidability of propositional separation logic and its neighbours

Cited in

(15)

• Proof tactics for assertions in separation logic
• Completeness and expressiveness of pointer program verification by separation logic
• Completeness proof by semantic diagrams for transitive closure of accessibility relation
• Completeness for a first-order abstract separation logic
• A Formalisation of Smallfoot in HOL
• Automated theorem proving for assertions in separation logic with all connectives
• scientific article; zbMATH DE number 1907992 (Why is no real title available?)
• A complete axiomatisation for quantifier-free separation logic
• Completeness for cut-based abduction
• Parametric completeness for separation theories
• Proof search for propositional abstract separation logics via labelled sequents
• A PSPACE-complete first-order fragment of computability logic
• Completion of first-order clauses with equality by strict superposition
• The logic of separation logic: models and proofs
• First-order hybrid separation logic

Describes a project that uses

Uses Software

• Smallfoot

This page was built for publication: Completeness for a first-order abstract separation logic

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