Automatic Verification of Concurrent Hardware and Software Systems

CCR-0098072 Edmund Clarke摘要：模型检查是一种用于并发系统的自动验证技术，例如时序电路设计和通信协议，其中通过对并发系统的状态空间的穷举搜索来检查时序逻辑规范。在过去的二十年里，已经取得了相当大的进展，许多大公司现在都在使用模型检查。为了扩展该方法的潜力，该项目追求几种研究途径，以使更大的硬件系统和某些软件系统能够被验证。模型检查和定理证明：定理证明避免了状态爆炸问题，但严重依赖于人类的指导，并且往往难以管理大型设计。 该项目试图找到并实现一种实用的方法，将联合收割机的定理证明和模型检测的好处，并将其应用到验证的处理器和安全protocol. SAT基于模型检测：最近开发的一种补充方法，传统的模型检测的基础上二叉决策图（BDDs），SAT求解器往往遭受较少的状态爆炸问题比BDDs。 本项目研究如何SAT求解器和BDD技术可以进一步整合，使验证更大的systems.Software模型检查：虽然模型检查的主要成功已经在硬件中，该程序最初是为软件开发的。 Clarke和Emerson在1981年的第一篇论文中提出了提取并发程序的同步骨架并对其进行模型检测的方法，模型检测的发展使人们对这种方法产生了新的兴趣。 本项目将探讨如何实现这一目标。

CCR-0098072Edmund ClarkeCMUABSTRACT:Model checking is an automatic verification technique for concurrent systems such as sequential circuit design and communication protocols in which temporal logic specifications are checked by an exhaustive search of the state space of the concurrent system. Considerable progress has been made in the last two decades, and many major companies are now using model checking. To extend the potential of the method, this project pursues several avenues of research that will enable larger hardware systems and certain software systems to be verified.Model Checking and theorem proving: Theorem proving avoids the state explosion problem, but relies heavily on human guidance and tends to get unmanageable for large designs. The project attempts to find and implement a practical methodology that will combine the benefits of theorem proving and model checking and apply it to verification of processors and security protocols.SAT-based Model Checking: Developed recently as a complementary approach to traditional model checking based on Binary Decision Diagrams (BDDs), SAT solvers tend to suffer less from the state explosion problem than BDDs. This project investigates how SAT solvers and BDD techniques can be further integrated to enable verification of larger systems.Software Model Checking: Although the major successes of model checking have been in hardware, the procedure was originally developed for software. The first paper by Clarke and Emerson in 1981 proposed extracting the synchronization skeleton of a concurrent program and model checking it. Advances in model checking have generated renewed interest in this approach. This project will explore how to achieve this goal.