Automatic Verification of Finite-State Concurrent Systems in Hardware and Software

9803774模型检查是一种有限状态并发系统的自动验证技术，如顺序电路设计和通信协议。通过使用像二进制决策图这样的特殊数据结构，可以验证具有大量可达状态的系统的属性。虽然这项技术已经开始被英特尔、摩托罗拉和西门子等公司使用，但要充分发挥这种方法的潜力，还需要进一步的研究。该项目将开发许多新技术，使大型硬件系统和某些类型的软件系统（如安全协议和概率程序）能够得到验证。新技术包括扩展偏序约简以允许实时程序的符号模型检查，将模型检查与定理证明相结合，使用程序切片来减少模型检查中的状态爆炸问题，以及将抽象与二元决策图相结合

9803774 Model Checking is an automatic verification technique for finite state concurrent systems such as sequential circuit designs and communication protocols. By using special data structures like Binary Decision Diagrams, it is possible to verify properties of systems with extremely large numbers of reachable states. Although the technique is beginning to be used by companies like Intel, Motorola, and Siemens, additional research is needed to realize the full potential of the method. This project will develop a number of new techniques that should enable larger hardware systems and certain types of software systems such as security protocols and probabilistic programs to be verified. The new techniques involve extending the partial order reduction to permit symbolic model checking of real-time programs, combining model checking and theorem proving, using program slicing to reduce the state explosion problem in model checking, and combining abstraction with binary decision diagrams.***