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.

By: Rachel Tzoref, Mark Matusevich, Eli Berger, Ilan Beer

Published in: Lecture Notes in Computer Science, volume 2860, (no ), pages 141-9 in 2003

Please obtain a copy of this paper from your local library. IBM cannot distribute this paper externally.

Questions about this service can be mailed to .