论文标题
S2TD：一个分离逻辑验证者，支持缺乏和存在错误的推理
S2TD: a Separation Logic Verifier that Supports Reasoning of the Absence and Presence of Bugs
论文作者
论文摘要
众所周知，堆肥计划是具有挑战性的。我们提出了一个新的验证器，用于使用S2TD的堆，该程序使用具有递归谓词和悬空谓词的分离逻辑（SL）的新型分离逻辑（SL）的新型扩展，以约束角条款（CHC）的形式系统地编码程序。 S2TD积极探索循环证明，以解决路径爆炸问题。 S2TD通过专注于堆肥程序并采用循环证明来有效地验证或通过反例验证它们，从而将自己与现有的基于CHC的验证者区分开来。与现有的基于SL的验证符相比，S2TD精确地指定了脱离分配的指针的堆，以避免误报误差，以推理存在错误的存在。 S2TD已使用SV-Comp存储库的一组全面的基准程序进行了评估。结果表明，S2TD比制作程序验证符更有效，并且比大多数人更有效。
Heap-manipulating programs are known to be challenging to reason about. We present a novel verifier for heap-manipulating programs called S2TD, which encodes programs systematically in the form of Constrained Horn Clauses (CHC) using a novel extension of separation logic (SL) with recursive predicates and dangling predicates. S2TD actively explores cyclic proofs to address the path explosion problem. S2TD differentiates itself from existing CHC-based verifiers by focusing on heap-manipulating programs and employing cyclic proof to efficiently verify or falsify them with counterexamples. Compared with existing SL-based verifiers, S2TD precisely specifies the heaps of de-allocated pointers to avoid false positives in reasoning about the presence of bugs. S2TD has been evaluated using a comprehensive set of benchmark programs from the SV-COMP repository. The results show that S2TD is more effective than state-of-art program verifiers and is more efficient than most of them.
