Boosting Automated Verification Using Cyclic Proof

基于分离逻辑的自动验证工具最近已经能够对扩展到数百万行的代码库进行验证。这种分析依赖于使用归纳谓词来描述存储在内存中的数据结构。然而，这些谓词目前是硬编码到分析中的，这意味着当遇到未知的数据结构时，分析必须失败，而这些数据结构不是硬编码定义所描述的。这导致了项目覆盖率的降低和假阴性率的增加。因此，用“一般”归纳定义的谓词进行推理的方法可以极大地提高技术水平。循环证明在本质上实现了对一般归纳定义的无限下降推理。传统的显式归纳法证明迫使证明者在证明的一开始就选择归纳模式和假设，与之相反，循环证明允许这些困难的决定被“推迟”，直到对证明搜索空间的探索使合适的选择更加明显。这使得循环证明成为一种有吸引力的自动证明搜索方法。本建议的主要论点是，循环证明技术可以增加归纳推理能力，对于一般归纳谓词，到程序间程序分析的许多组成部分（定理证明，溯因，框架推理，抽象），从而可以显着扩展当前验证方法的范围。

Automatic verification tools based on separation logic have recently enabled the verification of code bases that scale into the millions of lines. Such analyses rely on the use of *inductive predicates* to describe data structures held in memory. However, such predicates are currently hard-coded into the analysis, which means that the analysis must fail when encountering an unknown data structure, not described by the hard-coded definitions. This results in reduced program coverage and increased rates of false negatives. Thus, methods for reasoning with *general* inductively defined predicates could greatly enhance the state of the art.Cyclic proof, in essence, implements reasoning by infinite descent à la Fermat for general inductive definitions. In contrast to traditional proofs by explicit induction, which force the prover to select the induction schema and hypotheses at the very beginning of a proof, cyclic proof allows these difficult decisions to be *postponed* until exploration of the proof search space makes suitable choices more evident. This makes cyclic proof an attractive method for automatic proof search.The main contention of this proposal is that cyclic proof techniques can add inductive reasoning capability, for general inductive predicates, to the many components of an interprocedural program analysis (theorem proving, abduction, frame-inference, abstraction) and thus can significantly extend the reach of current verification methods.