QuTie: reasoning with Quantifiers and Theories

计算机和智能手机现在用于日常生活的各个领域，从商业到教育再到娱乐。从个人到国家一级，我们已经变得依赖软件系统，如果这些系统出现故障或其安全受到损害，我们就有可能遭受重大损失。防止这种情况的唯一方法是确保软件没有固有的弱点，这就需要我们使用数学的力量来证明软件是安全的。随着软件系统变得越来越复杂，失败的可能性也越来越大。传统的测试方法变得不可扩展，对软件系统的安全性提供较弱的保证。同样，我们的软件系统越来越多地受到那些试图利用我们对技术的依赖来达到自己邪恶目的的人的攻击。这些所谓的网络攻击正变得越来越复杂，积极寻求颠覆现有的检测方法。只有消除潜在的脆弱性，我们才能真正保护自己。因此，要正确处理安全性和安全性的概念，我们必须关注软件系统的基本属性，并对它们进行一般性的推理。存在用于检查软件系统的安全性和安全属性的各种方法。这些方法中的一个共同主题是在逻辑中描述软件的部分和所需的属性，并使用自动定理证明工具来检查属性是否成立。因此，对这种自动定理证明技术有很强的依赖性。该项目旨在解决该技术中的一个弱点，即它可以处理来自软件系统属性检查领域的各种问题。通过改进底层技术，我们的目标是对依赖于它的工具产生深远的影响。该项目的主要成果是对曼彻斯特开发的广泛使用的屡获殊荣的Vampire自动定理证明工具的一些扩展。通过使用Vampire作为这项研究的工具，我们相信我们将能够将基础研究的结果转化为实用，可用和有效的工具。

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.