Bounded model checking (BMC) is a procedure that searches for counterexamples to a given property through bounded executions of a non-terminating system. This paper compares the performance of SAT-based, BDD-based and explicit state based BMC on benchmarks drawn from commercial designs. Our experimental framework provides a uniform and comprehensive basis to evaluate each of these approaches. The experimental results in this paper suggest that for designs with deep counterexamples, BDD-based BMC is much faster. For designs with shallow counterexamples, we observe that indeed SAT-based BMC is more effective than BDD-based BMC, but we also observe that explicit state based BMC is comparably effective, a new observation. © Springer-Verlag Berlin Heidelberg 2003.
CITATION STYLE
Amla, N., Kurshan, R., McMillan, K. L., & Medel, R. (2003). Experimental analysis of different techniques for bounded model checking. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2619, 34–48. https://doi.org/10.1007/3-540-36577-x_4
Mendeley helps you to discover research relevant for your work.