EPSRC Reference: 
EP/V000209/1 
Title: 
CAPS: Collaborative Architectures for Proof Search 
Principal Investigator: 
Reger, Dr G 
Other Investigators: 

Researcher CoInvestigators: 

Project Partners: 

Department: 
Computer Science 
Organisation: 
University of Manchester, The 
Scheme: 
New Investigator Award 
Starts: 
01 July 2020 
Ends: 
14 July 2023 
Value (£): 
251,632

EPSRC Research Topic Classifications: 
Fundamentals of Computing 
Software Engineering 

EPSRC Industrial Sector Classifications: 
No relevance to Underpinning Sectors 


Related Grants: 

Panel History: 
Panel Date  Panel Name  Outcome 
20 May 2020

EPSRC ICT Prioritisation Panel May 2020

Announced


Summary on Grant Application Form 
What do a number theorist, a security analyst, and a data scientist have in common? They all have access to tools to help them, which at their core are powered by automated theorem provers. A number theorist can phrase her problem in a proof assistant and call on a socalled `hammer' to attempt to automatically prove the problem, or some part of it. A security analyst may execute a software model checker to ensure his code lacks certain vulnerabilities related to memory access. A data scientist may query a semantic database and generate an explanation for the result of her query. All these tools work by translating their problem to a series of subproblems to be solved by an automated theorem prover.
Whilst automated theorem provers have long been the workhorse for a variety of applications, there is a growing interest in the area of safe and secure software systems. As software systems grow more complex the potential for failure grows and traditional methods struggle to establish their safety, similarly, our software systems are increasingly subject to attacks from those who seek to exploit our dependence on technology for their own nefarious purposes. These socalled cyber attacks are becoming more elaborate, actively seeking to subvert existing methods of detection. Only by removing the underlying vulnerabilities can we truly protect ourselves. As described above, a common theme among approaches for checking safety and security properties of software systems is to describe parts of the software and desired property in logic and to use an automated theorem prover to check if the property holds. Therefore, there is a strong reliance on this automated theorem proving technology.
Automated theorem provers implement a method called `proof search' that uses a large array of heuristics to guide the prover towards a proof. Sets of heuristics are commonly collected together into strategies and it is widely observed that on a given problem one strategy may solve the problem quickly but another may diverge, never finding a solution. The consequence is that modern theorem provers utilise portfolios of strategies to tackle difficult problems, with the hope that one strategy will behave well. However, in the same way that different problems behave differently under different strategies, a problem can contain subproblems that behave differently under different strategies. Ideally, we would select different strategies at the subproblem level.
The CAPS project will develop a collaborative parallel architecture that allows multiple prover instances to work on the same problem, with different strategies being tried on different subproblems. This should have a synergistic effect. Consider a problem that is not provable by any single strategy in a portfolio but where each of its subproblems is. In such a case, an unprovable problem becomes provable. Furthermore, this new architecture offers a new opportunity for parallelism, something that does not fit naturally into the normal structure of proof search.
The main deliverable of this project is a novel collaborative parallel architecture implemented in the widelyused awardwinning Vampire automated theorem prover developed in Manchester. By using Vampire as a vehicle for this research we are confident that we will be able to translate the results of fundamental research into a practical, usable and impactful tool.

Key Findings 
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk

Potential use in nonacademic 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: 
http://www.man.ac.uk 