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.

Academic beneficiaries of the proposed project are covered in the section above.

The immediate non-academic beneficiaries of this proposal are organisations developing program verification technology based on separation logic and related formalisms. Two such organisations, Microsoft Research Cambridge and Monoidics Inc., are Project Partners on this proposal and have provided letters of support. They will benefit because we hope that the state-of-the-art inductive techniques for solving the individual problems that arise in a interprocedural program analysis based on separation logic - such as entailment, frame inference, and abduction - developed as the core contribution of this project can be integrated into these larger analyses, and used to improve them. Because we intend to reason using general inductive predicates rather than fixed predicates describing data structures as is the case currently, we hope that such integration will improve the coverage and automation of these analyses. Such an improvement would have a real and substantial im-
pact on the boundaries of the state of the art in automatic program verification, and might eventually lead to our techniques being taken up in industrial tools.

In wider society, the use of sophisticated and often buggy software to carry out everyday tasks is increasingly ubiquitous; for example, there are now more than 250,000,000 Android phones in current use. By improving the performance of automatic verification tools that will increasingly be used to verify such software, this project will help to catch memory leaks, null pointer dereferences and other critical bugs, and help to ensure that programs work as intended. Thus, if successful, this proposal could potentially yield a substantial indirect benefit for UK society at large.