Collaborative Research: Logical Support for Formal Verification

计算“证明助手”允许用户构造正式指定的断言的公理证明，目前用于两个目的：第一，验证普通的数学证明，第二，验证硬件和软件的（描述）是否符合设计规范。该项目将开发逻辑和计算方法来支持这两种类型的活动。该项目的具体组成部分包括：开发支持数论和离散几何证明的正式库；从软件组件规范和实现中提取验证条件，使用一种称为Resolve的自信编程语言；在这两个领域中出现的推理类型的分类；自动验证这些推论的逻辑方法的发展；教材和软件的开发将使这些方法整合到计算机科学和数学的本科和研究生课程中成为可能。随着数学证明变得越来越复杂，并且现在往往依赖于大量的计算，验证它们的正确性变得越来越困难。同样，随着硬件和软件系统变得越来越复杂，验证它们是否满足其设计规范也变得越来越困难。当资源、生命和安全依赖于他们的正确行为时，这样做尤为重要。数学逻辑学家和计算机科学家之间的这种合作将开发出各种方法，使验证这些数学和计算断言是有效的，以及支持它们的论证没有错误成为可能。该项目还将开发培训下一代计算机科学家和数学家使用这些方法的方法。

Computational "proof assistants," which allow users to construct axiomatic proofs of formally specified assertions, are currently used for two purposes: first, to verify ordinary mathematical proofs, and second, to verify that (descriptions of) hardware and software meet design specifications. This project will develop logical and computational methods to support both types of activities. Specific components of the project include: the development of formal libraries to support proofs in number theory and discrete geometry; the extraction of verification conditions from software component specifications and implementations in an assertive programming language known as Resolve; a classification of the types of inferences that arise in both domains; the development of logical methods for verifying these inferences automatically; and the development of educational materials and software that will make it possible to integrate these methods into undergraduate and graduate curricula in computer science and mathematics.As mathematical proofs become more and more intricate, and now often rely on extensive computation, it is becoming increasingly difficult to verify that they are correct. Similarly, as hardware and software systems become more and more complex, it is becoming increasingly difficult to verify that they meet their design specifications. Doing so is especially important when resources, lives, and security depend on their correct behavior. This collaboration between mathematical logicians and computer scientists will develop methods to make it possible to verify that such mathematical and computational claims are valid, and that the arguments supporting them are free of errors. The project will also develop means of training the next generation of computer scientists and mathematicians to use these methods.