Symbolic Model Checking without BDDs

Abstract

Symbolic Model Checking has proven to be a powerful technique for the verification of reactive systems. BDDs have traditionally been used as a symbolic representation of the system. We show how boolean decision procedures, like St{\aa}lmarck's Method or the Davis~\&~Putnam Procedure, 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 \emph{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 will be presented.