Automatic Verification of Concurrent Hardware and Software Systems

Carnegie Mellon University, Pittsburgh PA

Investigators

Abstract

CCR-0098072 Edmund Clarke CMU ABSTRACT: 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.