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.***