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.