Cyclic Proofs for Logic-Based Program Verification
Lead Research Organisation:
Imperial College London
Department Name: Computing
Abstract
The last few years have seen a increasingly widespreadinterest, both from the academic perspective and from elementsof industry, in the mathematical verification of desirableproperties of computer programs. Such properties might state,for example, that a program does not exceed its memory bounds(``memory safety'') or that it is always able to perform acertain action (``liveness''). The development of appropriatereasoning principles for programs and of proof systems andcomputer tools supporting those principles is thus currentlyattracting considerable activity amongst the computer scienceresearch community.Despite the advances in developing various forms of programlogic, the underlying notion of a *proof* of a programproperty has changed very little; by default, a proof is afinite tree whose construction respects the particularinference rules of the logic (a.k.a. derivation tree ), sothat the leaves of the tree are axiom instances and the root ofthe tree is the theorem to be proven, with intermediate nodesrelated by logical inferences. Recently, however, analternative mode of formal proof has been mooted as a paradigmfor reasoning in logics that feature various forms ofrecursion, known as *cyclic proof*. A cyclic proof isessentially obtained by identifying some cycles in a derivationtree, i.e., a cyclic proof is really a regular, infinitederivation tree, represented in cyclic graph form. Typically,not every such proof structure represents a sound proof, so anadditional, global guardedness condition is imposed oncyclic proofs that ensures their soundness. The existing investigations of cyclic proof, first in the purelogical settings of first-order logic and BI with inductivedefinitions, and subsequently in a separation logic systemfor proving termination of simple programs, have demonstratedits viability as a tool for formal reasoning, and its potentialpower as a proof method. Moreover, in the case of first-orderlogic with inductive definitions, a completeness result foran associated infinitary proof system establishes the semanticnaturality of the approach. We view our previous work in thesedirections as having substantially established the area ofcyclic proof as both a theoretically natural one worthy ofstudy, and ripe for applications in program verification.The broad aim of the proposed Postdoctoral Fellowship is tobuild on the developed theoretical foundations of cyclic proof,and especially its initial development into separationlogic-based reasoning about programs, in order to furtherexploit the ideas in the direction of applications. First, we wish to formulate and analyse cyclic proof systems for program verification based on separation logic, and to extend the cyclic proof concept to mixed induction and coinduction. Second, we wish to investigate the potential of cyclic proof as a vehicle for automated theorem proving.
People |
ORCID iD |
James Brotherston (Principal Investigator) |
Publications
Brotherston J
(2009)
Classical BI (A logic for reasoning about dualising resources)
Brotherston J
(2009)
Classical BI a logic for reasoning about dualising resources
in ACM SIGPLAN Notices
Brotherston J
(2011)
Automated Deduction - CADE-23
Brotherston J
(2012)
Bunched Logics Displayed
in Studia Logica
Brotherston J
(2010)
A Unified Display Proof Theory for Bunched Logic
Brotherston J
(2011)
Automated Reasoning with Analytic Tableaux and Related Methods
Brotherston J
(2010)
Classical BI: Its Semantics and Proof Theory
in Logical Methods in Computer Science
Brotherston J
(2010)
Undecidability of Propositional Separation Logic and Its Neighbours
Brotherston J
(2010)
Sequent calculi for induction and infinite descent
in Journal of Logic and Computation
Description | As well as the research on cyclic proofs highlighted in the original fellowship proposal, we identified several interesting and significant foundational issues concerning the resource-orientated logics (like separation logic) to which we had proposed applying cyclic proof technology, and were able to make progress in both areas. |
Exploitation Route | The Cyclist theorem prover, developed as part of the fellowship, is open source software and can be used for a wide range of user defined logics. |
Sectors | Digital/Communication/Information Technologies (including Software) |
Description | The papers produced as the principal outcome of this fellowship have since received multiple citations by authors working on related subjects. The Cyclist theorem prover is now a standard point of comparison for authors working on automated verification in separation logic (and in inductive theorem proving more generally). |
First Year Of Impact | 2012 |
Sector | Digital/Communication/Information Technologies (including Software) |
Description | Raj |
Organisation | Australian National University (ANU) |
Country | Australia |
Sector | Academic/University |
PI Contribution | Joint work on research project into Craig interpolation for displayable logics |
Collaborator Contribution | Joint work on research project into Craig interpolation for displayable logics |
Impact | TABLEAUX 2011 publication: Craig Interpolation for Displayable Logics by Brotherston and Gore. IJCAR 2016 publication: Machine-checked interpolation theorems for substructural logics using display calculi by Dawson, Brotherston and Gore |
Start Year | 2010 |
Title | Cyclist |
Description | Cyclic theorem proving framework instantiable to a wide range of user-defined logics. Comes with prebuilt instantiations and specialised auxiliary tools. |
Type Of Technology | Software |
Year Produced | 2012 |
Open Source License? | Yes |
Impact | We believe this to be the first general-purpose theorem proving tool based on the theoretical concept of "cyclic proof". |
URL | https://github.com/ngorogiannis/cyclist |