| EPSRC Reference: |
EP/V000209/1 |
| Title: |
CAPS: Collaborative Architectures for Proof Search |
| Principal Investigator: |
Reger, Dr G |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Computer Science |
| Organisation: |
University of Manchester, The |
| Scheme: |
New Investigator Award |
| Starts: |
01 July 2020 |
Ends: |
30 June 2022 |
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 so-called `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 sub-problems 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 so-called 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 sub-problems that behave differently under different strategies. Ideally, we would select different strategies at the sub-problem 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 sub-problems. 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 sub-problems 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 widely-used award-winning 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 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: |
http://www.man.ac.uk |