论文标题
分离逻辑片段中有效的循环支出程序
An Efficient Cyclic Entailment Procedure in a Fragment of Separation Logic
论文作者
论文摘要
有效的构成系统对使用分离逻辑的组成验证至关重要。不幸的是，现有的决策程序要么表现不佳或效率低下。例如，SmallFoot是一个有效的过程，但仅与硬连线列表和树一起使用。其他可以支持一般归纳谓词的程序会及时成倍地运行，因为他们的证明搜索需要对后跟踪来处理随之而来的脱节。 本文提出了一种决策程序，以在多项式时间内为一般电感谓词提供循环范围的证明。我们的程序效率很高，不需要后跟踪；它使用标准化规则，有助于避免在随后引入分离。此外，我们可决定的片段足以表达：它基于组成谓词，可以捕获广泛的数据结构，包括分类和嵌套的列表段，带有快速向前指针的跳过列表以及二进制搜索树。我们已经在原型工具中实施了该提案，并在最近的分离逻辑竞争中对挑战性问题进行了评估。实验结果证实了拟议系统的效率。
An efficient entailment proof system is essential to compositional verification using separation logic. Unfortunately, existing decision procedures are either inexpressive or inefficient. For example, Smallfoot is an efficient procedure but only works with hardwired lists and trees. Other procedures that can support general inductive predicates run exponentially in time as their proof search requires back-tracking to deal with a disjunction in the consequent. This paper presents a decision procedure to derive cyclic entailment proofs for general inductive predicates in polynomial time. Our procedure is efficient and does not require back-tracking; it uses normalisation rules that help avoid the introduction of disjunction in the consequent. Moreover, our decidable fragment is sufficiently expressive: It is based on compositional predicates and can capture a wide range of data structures, including sorted and nested list segments, skip lists with fast forward pointers, and binary search trees. We have implemented the proposal in a prototype tool and evaluated it over challenging problems taken from a recent separation logic competition. The experimental results confirm the efficiency of the proposed system.
