EPSRC logo

Details of Grant 

EPSRC Reference: EP/K040049/1
Title: Boosting Automated Verification Using Cyclic Proof
Principal Investigator: Brotherston, Dr J
Other Investigators:
Cook, Professor B
Researcher Co-Investigators:
Dr KN Gkorogiannis
Project Partners:
Microsoft Monoidics Ltd
Department: Computer Science
Organisation: UCL
Scheme: Standard Research
Starts: 11 November 2013 Ends: 10 May 2017 Value (£): 550,181
EPSRC Research Topic Classifications:
Fundamentals of Computing
EPSRC Industrial Sector Classifications:
Information Technologies
Related Grants:
Panel History:
Panel DatePanel NameOutcome
11 Apr 2013 EPSRC ICT Responsive Mode - Apr 2013 Announced
Summary on Grant Application Form
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.
Key Findings
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Potential use in non-academic contexts
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Impacts
Description This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Summary
Date Materialised
Sectors submitted by the Researcher
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Project URL:  
Further Information:  
Organisation Website: