An Optimized Symbolic Bounded Model Checking Engine

It has been shown that bounded model checking using a SAT solver can solve many verification problems that cause BDD based symbolic model checking engines to explode. However, no single algorithmic solution has proven to be totally superior in resolving all types of model checking problems. In this paper, we present an optimized bounded model checker which is based on BDDs, and describe the advantages and drawbacks of this model checker as compared to BDD-based symbolic model checking and SAT-based model checking. We show that, in some cases, this engine solves verification problems that could not be solved by other methods.