EPSRC logo

Details of Grant 

EPSRC Reference: EP/P03408X/1
Title: QuTie: reasoning with Quantifiers and Theories
Principal Investigator: Voronkov, Professor A
Other Investigators:
Reger, Dr G
Researcher Co-Investigators:
Project Partners:
Austrian Soc for Rigorous Systems Eng Max Planck Institutes (Grouped) Microsoft
Department: Computer Science
Organisation: University of Manchester, The
Scheme: Standard Research
Starts: 30 August 2017 Ends: 29 August 2020 Value (£): 359,372
EPSRC Research Topic Classifications:
Fundamentals of Computing
EPSRC Industrial Sector Classifications:
Information Technologies
Related Grants:
Panel History:
Panel DatePanel NameOutcome
19 Apr 2017 EPSRC ICT Prioritisation Panel April 2017 Announced
Summary on Grant Application Form
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.
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