Strong-separation logic

DOI10.1007/978-3-030-72019-3_24zbMATH Open1473.03015arXiv2001.06235OpenAlexW3151003345MaRDI QIDQ2233486FDOQ2233486

Authors: Jens Pagel, Florian Zuleger 

Publication date: 18 October 2021

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.

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

Recommendations

• On the almighty wand
• FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
• On the Almighty Wand
• Program Verification with Separation Logic
• A separation logic with data: small models and automation

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Logic in computer science (03B70)

Cites Work

• Deciding Entailments in Inductive Separation Logic with Tree Automata
• BI as an assertion language for mutable data structures
• Permission accounting in separation logic
• Programming Languages and Systems
• Resources, concurrency, and local reasoning
• A decision procedure for separation logic in SMT
• Separation Logic Modulo Theories
• Tractable Reasoning in a Fragment of Separation Logic
• On the almighty wand
• Title not available (Why is that?)
• FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
• Decidable logics combining heap structures and data
• The tree width of separation logic with recursive definitions
• Compositional Shape Analysis by Means of Bi-Abduction
• Program Logics for Certified Compilers
• The effects of adding reachability predicates in propositional separation logic
• Strong-separation logic
• A Complete Decision Procedure for Linearly Compositional Separation Logic with Data Constraints
• A separation logic with data: small models and automation
• Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic
• Separation Logic with Monadic Inductive Definitions and Implicit Existentials
• Foundations for Decision Problems in Separation Logic with General Inductive Predicates
• A decidable fragment in separation logic with inductive predicates and arithmetic
• The Bernays-Schönfinkel-Ramsey class of separation logic on arbitrary domains
• Expressive completeness of separation logic with two variables and no separating conjunction
• Separation Logic with One Quantified Variable

Cited In (7)

• Weak updates and separation logic
• Fluid updates: beyond strong vs. weak updates
• Sound Automation of Magic Wands
• The strong version of a sentential logic
• 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)