Symbolic Model Checking without BDDs

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 Stålmarck'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.