Abstract: Most automated verifiers for separation logic target the symbolic-heap fragment, disallowing both the magic-wand operator and the application of classical Boolean operators to spatial formulas. This is not surprising, as support for the magic wand quickly leads to undecidability, especially when combined with inductive predicates for reasoning about data structures. To circumvent these undecidability results, we propose to assign a more restrictive semantics to the separating conjunction. We argue that the resulting logic, strong-separation logic, can be used for compositional program verification and bi-abductive static analysis just like "standard" separation logic, while remaining decidable even in the presence of both the magic wand and the list-segment predicate -- a combination of features that leads to undecidability assuming the standard semantics.
Recommendations
Cites work
- scientific article; zbMATH DE number 2081098 (Why is no real title available?)
- A complete decision procedure for linearly compositional separation logic with data constraints
- A decidable fragment in separation logic with inductive predicates and arithmetic
- A decision procedure for separation logic in SMT
- A separation logic with data: small models and automation
- BI as an assertion language for mutable data structures
- Compositional shape analysis by means of bi-abduction
- Decidable logics combining heap structures and data
- Deciding entailments in inductive separation logic with tree automata
- Expressive completeness of separation logic with two variables and no separating conjunction
- FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
- Foundations for decision problems in separation logic with general inductive predicates
- On the almighty wand
- Permission accounting in separation logic
- Program logics for certified compilers
- Programming Languages and Systems
- Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic
- Resources, concurrency, and local reasoning
- Separation logic modulo theories
- Separation logic with monadic inductive definitions and implicit existentials
- Separation logic with one quantified variable
- Strong-separation logic
- The Bernays-Schönfinkel-Ramsey class of separation logic on arbitrary domains
- The effects of adding reachability predicates in propositional separation logic
- The tree width of separation logic with recursive definitions
- Tractable Reasoning in a Fragment of Separation Logic
Cited in
(8)- Unified reasoning about robustness properties of symbolic-heap separation logic
- Weak updates and separation logic
- Fluid updates: beyond strong vs. weak updates
- The strong version of a sentential logic
- Sound Automation of Magic Wands
- Programming Languages and Systems
- Strong-separation logic
- Transitive Separation Logic
This page was built for publication: Strong-separation logic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2233486)
