Complete Entailment Checking for Separation Logic with Inductive Definitions
share
In [A], we proposed a novel decision procedure for entailment checking in the symbolic-heap segment of separation logic with user-defined inductive definitions of bounded treewidth. In the meantime, we discovered that the decision procedure in [A] is incomplete. In this article, we fix the incompleteness issues while retaining the double-exponential asymptotic complexity bound. In doing so, we also remove several of the simplifying assumptions made in [A]. Furthermore, we generalize our decision procedure to the fragment of positive formulas, in which conjunction, disjunction, guarded negation and septraction can be freely combined with the separating conjunction. [A] Jens Katelaan, Christoph Matheja, and Florian Zuleger. Effective entailment checking for separation logic with inductive definitions. In Tomás Vojnar and Lijun Zhang, editors, Tools and Algorithms for the Construction and Analysis of Systems - 25th International Conference, TACAS 2019
READ FULL TEXT