Abstract
Bounded Model Checking based on SAT methods has recently been introduced as a complementary technique to BDD-based Symbolic Model Checking. The basic idea is to search for a counter example in executions whose length is bounded by some integer k. The BMC problem can be efficiently reduced to a propositional satisfiability problem, and can therefore be solved by SAT methods rather than BDDs. SAT procedures are based on general-purpose heuristics that are designed for any propositional formula. We show that the unique characteristics of BMC formulas can be exploited for a variety of optimizations in the SAT checking procedure. Experiments with these optimizations on real designs proved their efficiency in many of the hard test cases, comparing to both the standard SAT procedure and a BDD-based model checker.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Beer, I., Ben-David, S., Eisner, C., Geist, D., Gluhovsky, L., Heyman, T., Landver, A., Paanah, P., Rodeh, Y., Ronin, G., Wolfsthal, Y.: RuleBase: Model checking at IBM. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 480–483. Springer, Heidelberg (1997)
Beer, I., Ben-David, S., Eisner, C., Landver, A.: RuleBase: An industry oriented formal verification tool. In: Proc. Design Automation Conference 1996, DAC 1996 (1996)
Beer, I., Ben-David, S., Landver, A.: On-the-fly model checking of RCTL formulas. In: Hu, A.J., Vardi, M.Y. (ed.) CAV 1998. LNCS, vol. 1427, pp. 184–194. Springer, Heidelberg (1998)
Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, p. 193. Springer, Heidelberg (1999)
Biere, A., Clarke, E., Raimi, R., Zhu, Y.: Verifying safety properties of a powerPCTM microprocessor using symbolic model checking without bDDs. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 60–71. Springer, Heidelberg (1999)
Chan, W., Anderson, R., Beame, P., Notkin, D.: Improving efficiency of symbolic model checking for state-based system requirements. In: International Symposium on Software Testing and Analysis (ISSTA 1998). LNCS. Springer, Heidelberg (1998)
Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM 7, 201–215 (1960)
Iwashita, H., Nakata, T., Hirose, F.: Ctl model checking based on forward state traversal. In: IEEE/ACM International conference on Computer Aided Design, pp. 82–87 (November 1996)
Shtrichman, O.: Tuning sat checkers for bounded model checking - experiments with static and dynamic orderings. Technical report, Weizmann Institute (2000), can be downloaded from http://www.weizmann.ac.il/~ofers
Silva, J.P.M.: The impact of branching heuristics in propositional satisfiability algorithms. In: Barahona, P., Alferes, J.J. (eds.) EPIA 1999. LNCS (LNAI), vol. 1695, pp. 62–74. Springer, Heidelberg (1999)
Silva, J.P.M., Sakallah, K.A.: GRASP - a new search algorithm for satisfyability. Technical Report TR-CSE-292996, Univerisity of Michigen (1996)
Silva, J.P.M., Sakallah, K.A.: GRASP: A search algorithm for propositional satisfiability. IEEE Transactions on Computers 48, 506–516 (1999)
Zhang, H.: SATO: An efficient propositional prover. In: McCune, W. (ed.) CADE 1997. LNCS, vol. 1249. Springer, Heidelberg (1997)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Shtrichman, O. (2000). Tuning SAT Checkers for Bounded Model Checking. In: Emerson, E.A., Sistla, A.P. (eds) Computer Aided Verification. CAV 2000. Lecture Notes in Computer Science, vol 1855. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10722167_36
Download citation
DOI: https://doi.org/10.1007/10722167_36
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67770-3
Online ISBN: 978-3-540-45047-4
eBook Packages: Springer Book Archive