Bounded Model Checking Using Satisfiability Solving |
| |
Authors: | Edmund Clarke Armin Biere Richard Raimi Yunshan Zhu |
| |
Affiliation: | (1) Computer Science Department, CMU, 5000 Forbes Avenue, Pittsburgh, PA 15213, USA;(2) Institute of Computer Systems, ETH Zürich, 8092 Zürich, Switzerland;(3) TriMedia Technologies, Inc., 801 Capital of Texas Hwy. So., Austin, TX, 78704 |
| |
Abstract: | The phrase model checking refers to algorithms for exploring the state space of a transition system to determine if it obeys a specification of its intended behavior. These algorithms can perform exhaustive verification in a highly automatic manner, and, thus, have attracted much interest in industry. Model checking programs are now being commercially marketed. However, model checking has been held back by the state explosion problem, which is the problem that the number of states in a system grows exponentially in the number of system components. Much research has been devoted to ameliorating this problem.In this tutorial, we first give a brief overview of the history of model checking to date, and then focus on recent techniques that combine model checking with satisfiability solving. These techniques, known as bounded model checking, do a very fast exploration of the state space, and for some types of problems seem to offer large performance improvements over previous approaches. We review experiments with bounded model checking on both public domain and industrial designs, and propose a methodology for applying the technique in industry for invariance checking. We then summarize the pros and cons of this new technology and discuss future research efforts to extend its capabilities. |
| |
Keywords: | model checking processor verification satisfiability bounded model checking cone of influence reduction |
本文献已被 SpringerLink 等数据库收录! |
|