Collaborative Research: Logical Support for Formal Verification

协作研究：形式验证的逻辑支持

• 批准号: 0701260
• 负责人: Bruce Weide
• 金额: $ 7.5万
• 依托单位: Ohio State University Research Foundation -DO NOT USE
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2007
• 资助国家: 美国
• 起止时间: 2007-09-01 至 2010-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0701260&HistoricalAwards=false
• 关键词: Collaborative; Research; Logical; Support; Formal

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.

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