Temporal Logic, Hardware Verification, and Parallel Theorem Proving

时态逻辑、硬件验证和并行定理证明

• 批准号: 9005992
• 负责人: Edmund Clarke
• 金额: $ 21.2万
• 依托单位: Carnegie-Mellon University
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 1990
• 资助国家: 美国
• 起止时间: 1990-08-01 至 1993-01-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9005992&HistoricalAwards=false
• 关键词: Temporal; Logic; Hardware; Verification; Parallel

A procedure, called temporal logic model checking, for automatic verification of concurrent programs has been developed. This procedure determines if a collection of finite-state processes satisfies its specification in a propositional temporal logic by methodically searching the global state graph determined by the processes. The first part of this project deals with temporal logic model checking and how it can be extended to verify hardware controllers, cache coherency protocols, and real-time programs. In particular, new techniques (various methods for compositional model checking, alternative state space representations using binary decision graphs and partial orders, etc.) will be developed to extend the size of the finite state programs that can be handled using this technique. The second part of this project deals with parallel theorem proving and symbolic computation. A parallel resolution theorem prover called Parthenon has been built. In this project, a number of important algorithms for theorem proving and symbolic computation will be implemented on different types of multiprocessors.

开发了一种称为时态逻辑模型检验的并发程序自动验证过程。该过程通过有条不紊地搜索由进程确定的全局状态图来确定有限状态进程集合是否满足其在命题时态逻辑中的规范。本项目的第一部分涉及时态逻辑模型检查，以及如何将其扩展到验证硬件控制器、高速缓存一致性协议和实时程序。特别是，新技术(用于组合模型检查的各种方法、使用二元决策图和偏序的替代状态空间表示等)。将被开发来扩展可以使用该技术处理的有限状态程序的大小。该项目的第二部分涉及并行定理证明和符号计算。建立了一个并行归结定理证明器Parthenon。在这个项目中，一些重要的定理证明和符号计算算法将在不同类型的多处理器上实现。