A Decision Procedure for Guarded Separation Logic: Complete Entailment Checking for Separation Logic with Inductive Definitions

Christoph Matheja, Jens Pagel, Florian Zuleger

Research output: Contribution to journalJournal articleResearchpeer-review

134 Downloads (Pure)

Abstract

We develop a doubly exponential decision procedure for the satisfiability problem of guarded separation logic—a novel fragment of separation logic featuring user-supplied inductive predicates, Boolean connectives, and separating connectives, including restricted (guarded) versions of negation, magic wand, and septraction. Moreover, we show that dropping the guards for any of the preceding connectives leads to an undecidable fragment.
We further apply our decision procedure to reason about entailments in the popular symbolic heap fragment of separation logic. In particular, we obtain a doubly exponential decision procedure for entailments between (quantifier-free) symbolic heaps with inductive predicate definitions of bounded treewidth (SLbtw)—one of the most expressive decidable fragments of separation logic. Together with the recently shown2ExpTime-hardness for entailments in said fragment, we conclude that the entailment problem for SLbtw is 2ExpTime-complete—thereby closing a previously open complexity gap.
Original languageEnglish
Article number1
JournalACM Transactions on Computational Logic
Volume24
Issue number1
Number of pages76
ISSN1529-3785
DOIs
Publication statusPublished - 2023

Keywords

  • Decision procedures
  • Entailment
  • Magic wands
  • Inductive predicates

Fingerprint

Dive into the research topics of 'A Decision Procedure for Guarded Separation Logic: Complete Entailment Checking for Separation Logic with Inductive Definitions'. Together they form a unique fingerprint.

Cite this