Symbolic Model Checking without BDDs Export

@misc{citeulike:5860292, abstract = {Symbolic Model Checking [3, 14] has proven to be a powerful technique for the verification of reactive systems. BDDs [2] have traditionally been used as a symbolic representation of the system. In this paper we show how boolean decision procedures, like Stalmarck\&\#039;s Method [16] or the Davis \& Putnam Procedure [7], can replace BDDs. This new technique avoids the space blow up of BDDs, generates counterexamples much faster, and sometimes speeds up the verification. In addition, it produces counterexamples of minimal length. We introduce a bounded model checking procedure for LTL which reduces model checking to propositional satisfiability. We show that bounded LTL model checking can be done without a tableau construction. We have implemented a model checker BMC, based on bounded model checking, and preliminary results are presented. 1 Introduction Model checking [4] is a powerful technique for verifying reactive systems. Able to find subtle errors in real commercial designs, it is g...}, author = {Biere, Armin and Cimatti, Alessandro and Clarke, Edmund and Zhu, Yunshan}, citeulike-article-id = {5860292}, citeulike-linkout-0 = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.47.6709}, keywords = {model\_checker, model\_checking}, posted-at = {2009-11-10 20:26:18}, priority = {2}, title = {Symbolic Model Checking without BDDs}, url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.47.6709}, year = {1999} }

TY - ELEC ID - citeulike:5860292 L3 - citeulike-article-id:5860292 N2 - Symbolic Model Checking [3, 14] has proven to be a powerful technique for the verification of reactive systems. BDDs [2] have traditionally been used as a symbolic representation of the system. In this paper we show how boolean decision procedures, like Stalmarck's Method [16] or the Davis & Putnam Procedure [7], can replace BDDs. This new technique avoids the space blow up of BDDs, generates counterexamples much faster, and sometimes speeds up the verification. In addition, it produces counterexamples of minimal length. We introduce a bounded model checking procedure for LTL which reduces model checking to propositional satisfiability. We show that bounded LTL model checking can be done without a tableau construction. We have implemented a model checker BMC, based on bounded model checking, and preliminary results are presented. 1 Introduction Model checking [4] is a powerful technique for verifying reactive systems. Able to find subtle errors in real commercial designs, it is g... TI - Symbolic Model Checking without BDDs KW - model_checker KW - model_checking AU - Biere, Armin AU - Cimatti, Alessandro AU - Clarke, Edmund AU - Zhu, Yunshan PY - 1999/// UR - http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.47.6709 ER -