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.