Boosting Automated Verification Using Cyclic Proof
Lead Research Organisation:
University College London
Department Name: Computer Science
Abstract
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.
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.
Planned Impact
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.
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.
Publications
Brotherston J
(2016)
Model checking for symbolic-heap separation logic with inductive predicates
in ACM SIGPLAN Notices
Brotherston J
(2016)
Model checking for symbolic-heap separation logic with inductive predicates
Brotherston J
(2014)
Static Analysis
Kanovich M
(2016)
Logical Foundations of Computer Science
Brotherston J
(2015)
Automated Reasoning with Analytic Tableaux and Related Methods
Description | Separation logic is perhaps one of the greatest success stories in automatic program verification in recent history. Over the last 15 years, it has evolved from a novel way of reasoning about pointers in computer memory to a mainstream technique for scalable verification of software written in languages like C or Java, capable of treating programs of millions of lines of code. It now forms the basis of the INFER verifier now in widespread use at Facebook. The project aims to extend the reach of separation logic by automating its extension with inductively defined predicates, used to describe data structures in the memory. This had both a theoretical component, aiming to discover what is within reach of automation, and a practical component, aiming to implement our methods in software. In particular, we aim to build upon *cyclic proof* technology developed by the PI and collaborators. On the theoretical side, we established the decidability (with complexity bounds) of the model checking and satisfiability problems for separation logic with inductive predicates. On the other hand, we showed that many commonly assumed properties of separation logic models are in fact not propositionally axiomatisable, but that they become axiomatisable when one adds a notion of "naming", as used in hybrid logic. On the practical side, we provided implementations of the aforementioned decision procedures, and developed our theorem proving Cyclist to extend the reach of what can be verified automatically; in particular, a recent paper at CPP'17 demonstrated the power of our technique and implementation for establishing program termination. Further papers in this area are in development. |
Exploitation Route | Facebook is providing funding to and actively pursuing research collaborations with the PI. At the same time, the automated verification community, especially the subcommunity working on separation logic, is widely citing, competing with and building upon our research results. |
Sectors | Digital/Communication/Information Technologies (including Software) |
Description | Facebook Faculty Grant 2015 |
Amount | $30,000 (USD) |
Organisation | |
Sector | Private |
Country | United States |
Start | 10/2015 |
End | 09/2018 |
Description | Nikos |
Organisation | Middlesex University |
Country | United Kingdom |
Sector | Academic/University |
PI Contribution | Ongoing academic research collaboration |
Collaborator Contribution | Ongoing academic research collaboration |
Impact | CSL-LICS 2014 paper "A Decision Procedure for Satisfiability in Separation Logic with Inductive Predicates" SAS'14 paper "Cyclic Abduction of Inductively Defined Safety and Termination Preconditions" Cyclist theorem prover |
Start Year | 2013 |
Title | Cyclist 2014 |
Description | Updated the Cyclist theorem prover with substantial new techniques and features, as described in related publications. |
Type Of Technology | Software |
Year Produced | 2014 |
Open Source License? | Yes |
Impact | Cyclist was entered into and performed well in the new SL-COMP competition for separation logic theorem provers. |
URL | https://github.com/ngorogiannis/cyclist |
Title | SL disprover |
Description | Given an entailment A |= B between two formulas in separation logic with inductive predicates, this tool attempts to disprove the entailment, i.e. to infer the existence of a countermodel. |
Type Of Technology | Software |
Year Produced | 2014 |
Open Source License? | Yes |
Impact | First disprover for separation logic. Opens up potential new applications in speeding up verification and automatic proof search, and in automated theory exploration. |
URL | https://github.com/ngorogiannis/cyclist |
Title | SL model checker |
Description | Compares the heap memory of a running program against an assertion written in separation logic with general inductive definitions. |
Type Of Technology | Software |
Year Produced | 2015 |
Open Source License? | Yes |
Impact | First model checker of its kind, with potential applications to verification and software testing. |
URL | https://github.com/ngorogiannis/cyclist |