It has been shown that bounded model checking using a SAT solver can solve many verification problems that would 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. We present an optimized bounded model checker 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. © Springer-Verlag Berlin Heidelberg 2003.
CITATION STYLE
Tzoref, R., Matusevich, M., Berger, E., & Beer, I. (2003). An optimized symbolic bounded model checking engine. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2860, 141–149. https://doi.org/10.1007/978-3-540-39724-3_13
Mendeley helps you to discover research relevant for your work.