Abstract
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.
Chapter PDF
References
P. Bjesse and K. Claessen. SAT-based verification without state space traversal. In FMCAD, 2000.
A. Biere, A. Cimatti, E. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In Tools and Algorithms for the Construction and Analysis of Systems, volume 1579 of LNCS, 1999.
J. R. Burch, E. M. Clarke, K. L. McMillan, D.L. Dill, and J. Hwang. Symbolic model checking: 1020 states and beyond. In LICS, 1990.
A. Biere, E. Clarke, R. Raimi, and Y. Zhu. Verifying safety properties of a PowerPC microprocessor using symbolic model checking without BDDs. In CAV, 1999.
R. Brayton, G. Hachtel, A. Sangiovanni-Vincentelli, F. Somenzi, A. Aziz, S. Cheng, S. Edwards, S. Khatri, Y. Kukimoto, A. Pardo, S. Qadeer, R. Ranjan, S. Sarwary, T. Shiple, G. Swamy, and T. Villa. VIS. In FMCAD, 1996.
P. Bjesse, T. Leonard, and A. Mokkedem. Finding bugs in an Alpha microprocessor using satisfiability solvers. In CAV, volume 2102 of LNCS, 2001.
A. Boralv. The industrial success of verification tools based on stalmarck’s method. In CAV, 1997.
R. E. Bryant. Graph-based algorithms for boolean function manipulations. IEEE Transactions on Computers, 1986.
G. Cabodi, P. Camurati, and S. Quer. Can bdds compete with sat solvers on bounded model checking. In DAC, 2002.
E.M. Clarke and E. A. Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. In Workshop on Logics of Programs, volume 131 of LNCS, 1981.
Fady C., L. Fix, R. Fraer, E. Giunchiglia, G. Kamhi, A. Tacchella, and M. Y. Vardi. Benefits of bounded model checking at an industrial setting. In CAV, volume 2102 of LNCS, 2001.
E. Goldberg and Y. Novikov. Berkmin: A fast and robust sat-solver. In DATE, 2002.
Z. Har’El and R. P. Kurshan. Software for analytical development of communications protocols. AT&T Technical Journal, 69(1), 1990.
A. Kuehlmann and F. Krohm. Equivalence checking using cuts and heaps. In DAC, 1997.
D. Kroening and O. Strichman. Efficient computation of recurrence diameters. In VMCAI, 2002.
R. Kurshan. Computer-aided Verification of Coordinating Processes: The Automata-Theoretic Approach. Princeton University Press, 1994.
K. McMillan. Symbolic model checking: An approach to the state explosion problem. Kluwer Academic Publishers, 1993.
K. McMillan. Getting started with smv, 1999. URL: http://www-cad.eecs.berkeley.edu/~kenmcmil.
M. W. Moskewicz, C. F. Madigan, Y. Zhao, L. Zhang, and S. Malik. Cha.: Engineering an Efficient SAT Solver. In Proceedings of the 38th Design Automation Conference (DAC’01), 2001.
Marques-Silva and Sakallah. GRASP: A search algorithm for propositional satisfiability. IEEETC: IEEE Transactions on Computers, 48, 1999.
J.P. Queille and J. Sifakis. Specification and verification of concurrent systems in CESAR. In Proc. of the 5th International Symposium on Programming, volume 137 of LNCS, 1982.
M. Sheeran and G. Stålmarck. A tutorial on Stålmarck’s proof procedure for propositional logic. In CAV, volume 1522 of LNCS, 1998.
O. Strichman. Tuning SAT checkers for bounded model checking. In CAV, 2000.
M. N. Velev and R. E. Bryant. Effective use of boolean satisfiability procedures in the formal verification of superscalar and VLIW. In Proceedings of the 38th Conference on Design Automation Conference 2001, 2001.
H. Zhang. SATO: An eficient propositional prover. In Proceedings of the 14th International Conference on Automated deduction, volume 1249 of LNAI, 1997.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Amla, N., Kurshan, R., McMillan, K.L., Medel, R. (2003). Experimental Analysis of Different Techniques for Bounded Model Checking. In: Garavel, H., Hatcliff, J. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2003. Lecture Notes in Computer Science, vol 2619. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36577-X_4
Download citation
DOI: https://doi.org/10.1007/3-540-36577-X_4
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-00898-9
Online ISBN: 978-3-540-36577-8
eBook Packages: Springer Book Archive