论文标题
守卫分离逻辑的决策程序：与归纳定义的分离逻辑的完整需要检查
A Decision Procedure for Guarded Separation Logic: Complete Entailment Checking for Separation Logic with Inductive Definitions
论文作者
论文摘要
我们为守卫分离逻辑的满足性问题开发了一个双重指定的决策程序 - 一种新型的分离逻辑片段，具有用户提供的归纳谓词，布尔连接剂和分离连接剂，包括受限（受保护的）否定版本，否定版本，魔术wand和septraction。此外，我们表明，放下上述任何连接剂的警卫会导致不可能确定的碎片。我们进一步应用决策程序来理解分离逻辑的流行符号堆碎片中的索引。特别是，我们获得了一个双重指数的决策程序，用于（无量词）符号堆之间具有有限制的树宽（SLIDBTW）的诱导性谓词定义（SLIDBTW） - 分离逻辑中最表达的可决定性片段之一。加上最近显示的2次段落片段中的2次限制，我们得出结论，SlidBTW的累及问题是2Exptime-Complete-从而缩小了先前开放的复杂性差距。
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 above 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 (SLIDbtw) - one of the most expressive decidable fragments of separation logic. Together with the recently shown 2ExpTime-hardness for entailments in said fragment, we conclude that the entailment problem for SLIDbtw is 2ExpTime-complete - thereby closing a previously open complexity gap.
