CAPS: Collaborative Architectures for Proof Search

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.

There is a growing trend in many areas of computer science, in particular in program analysis and verification, to formulate a particular problem in terms of a number of sub-problems that can be automatically discharged by theorem provers. There is a wide range of applications of this approach, from checking security protocols to debugging device drivers, from answering semantic queries to aiding proof assistants. However, the most ubiquitous language for describing such problems (first-order logic) is undecidable in general and building theorem provers able to handle large and complex problems remains an active research problem. It is now widely accepted that there is no 'silver bullet' approach to theorem proving and most modern theorem provers employ portfolios of strategies. However, the standard architecture for theorem provers cannot make full use of this large set of strategies as it must select one strategy for a given problem and may not try different strategies on different sub-problems. CAPS will introduce a new architecture to remedy this.

The potential beneficiaries of CAPS include those developing similar tools, as they would be able to learn from these developments, but more prominently beneficiaries include those making use of Vampire (the vehicle for this research) in various ways. Vampire is currently used as a back-end solver in a number of other tools. For example, it has proved useful in the Sledgehammer tool for the Isabelle interactive theorem prover, and is available as a solver in the Why3 platform for program verification, which is itself used as a backend for systems such as Frama-C and SPARK. Therefore, we expect improvements in the power and efficiency of Vampire to have a large impact on this large tool space, making a significant contribution to national and international efforts to produce safe and secure software systems.

To achieve these benefits we will first follow the standard routes of publishing our results in world-leading conferences and journals. In addition to this, we will develop, provide and support an industrial-strength tool - a collaborative, parallel Vampire. The ecosystem we provide around Vampire is important for impact; the tool is hosted in an online repository and welcomes contributions from international researchers; Vampire regularly participate in international competitions, which provide a platform to demonstrate and advertise the system's capabilities; and we work closely with those using Vampire in their own work, allowing us to react to their needs. We will continue and extend all of these activities within the project.

As well as building on our existing successes we will also be reaching out to new communities, and industrial partners, to encourage them to take advantage of the powerful theorem proving resource. To achieve this we will (i) host a user-focussed workshop at the University of Manchester, (ii) run a tutorial at a leading software engineering or programming languages conference aimed at demonstrating the capabilities of Vampire and the potential applications within their fields of research, and (iii) carry out summer engineering projects to improve the usability of Vampire.

The impacts discussed so far are short to medium term. In the long term, this research contributes to a community effort to build safe and secure software systems, which are now integrated into our everyday lives. Theorem proving technology has the power, through utilisation by other tools, to transform the reliability, safety, security and usability of both safety-critical software such as traffic control systems and everyday applications such as device drivers on desktop computers. This project presents a significant contribution to this international long-term effort.