QuTie: reasoning with Quantifiers and Theories

Computers and smart phones are now used in all areas of everyday life, from business to education to entertainment. From the individual to the national level, we have become reliant on software systems and risk substantial loss if these systems fail or have their security compromised. The only way to protect against this is to ensure that the software has no inherent weakness, and this requires that we use the power of mathematics to prove that the software is both safe and secure.

As software systems grow more complex the potential for failure grows. Traditional testing approaches become unscalable and give weaker assurances about the safety of software systems. 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. Therefore, to properly handle notions of safety and security we must focus on fundamental properties of software systems and reason about them generally.

There exist various approaches for checking safety and security properties of software systems. A common theme among these approaches is to describe parts of the software and desired property in logic and to use an automated theorem proving tool to check if the property holds. Therefore, there is a strong reliance on this automated theorem proving technology. This project aims to address a weakness in this technology with respect to the kinds of problems it can deal with coming from this domain of checking properties of software systems. By improving the underlying technology we aim to have far-reaching impact on the tools that rely on it.

The main deliverable of this project is a number of extensions to the widely-used award-winning Vampire automated theorem proving tool 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 are a wide range of applications of this approach, from checking security protocols to debugging device drivers. Further progress in this direction is hindered by a lack of powerful methods able to efficiently handle theories such as arithmetic in combination with quantifiers (necessary to reason about constructs such as data structures). Developing such methods within the Vampire theorem prover is the focus of this project.

The potential beneficiaries of this project 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 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 improved methods for reasoning with quantifiers and theories implemented in 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 firstly follow the standard routes of publishing our results in world-leading conferences and journals. In addition to this we will develop, provide and support world-leading tools (notably Vampire) for reasoning with quantifiers and theories. The ecosystem we provide around Vampire is important for impact; we regularly participate in international competitions, which provide a platform to demonstrate and advertise the system's capabilities; we work closely with those using Vampire in their own work, allowing us to react to their needs; and we have productive and active collaborations with industrial partners, such as Microsoft Research and Dassault Aviation, giving us access to industrial level requirements and problems. 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 to encourage them to take advantage of the powerful theorem proving resource. To achieve this we will 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.

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.