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. In this paper we show how boolean decision procedures, like Stillmarck's Method or the Davis and 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 bounded model checking procedure for Lit which reduces model checking to propositional satisfiability. We show that bounded Lit model checking can be done without a tableau construction. We have implemented a model checkerBMC, based on bounded model checking, and preliminary results are presented.
Document Details
- Document Type
- Technical Report
- Publication Date
- Jan 04, 1999
- Accession Number
- ADA360973
Entities
People
- Alessandro Cimatti
- Armin Biere
- Edmund Clark
- Yunshan Zhu
Organizations
- Carnegie Mellon University