Temporal Logic, Hardware Verification, and Parallel Theorem Proving

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

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.