Collaborative research: logical support for formal verification

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

• 批准号: 0700174
• 负责人: Jeremy Avigad
• 金额: $ 21.77万
• 依托单位: Carnegie-Mellon University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2007
• 资助国家: 美国
• 起止时间: 2007-09-01 至 2010-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0700174&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的断言编程语言实现;对这两个领域中出现的推理类型进行分类;开发自动验证这些推理的逻辑方法;以及开发教材和软件，使这些方法有可能融入计算机科学和数学的本科生和研究生课程中。随着数学证明变得越来越复杂，现在往往依赖于广泛的计算，验证它们是否正确变得越来越困难。类似地，随着硬件和软件系统变得越来越复杂，验证它们是否满足其设计规范变得越来越困难。当资源、生命和安全取决于他们的正确行为时，这样做尤其重要。数学逻辑学家和计算机科学家之间的这种合作将开发方法，使人们有可能验证这种数学和计算索赔是有效的，并且支持它们的论点是没有错误的。该项目还将开发培训下一代计算机科学家和数学家使用这些方法的手段。