Abstract
The usefulness of Bounded Model Checking(BMC) based on propositional satisfiability methods has recently proven its efficacy for bug hunting. The basic idea is to search for a counterexample in executions whose length is bounded by some integer k. In fact, for some properties some bounded paths are equivalent. In the original Bounded Model Checking equivalent bounded paths may be searched repeatedly. Therefore some searches are redundant. In this paper with respect to some properties we exploit new encoding for Bounded Model Checking such that we can avoid searching for redundant bounded paths.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Clarke, E.M., Grumberg, O., Peled, D.: Model checking. MIT Press, Cambridge (2000)
Ben-Ari, M., Manna, Z., Pnueli, A.: The temporal logic of branching time. Acta Information 20, 207–226 (1983)
Pnueli, A.: A temporal logic of concurrent programs. Theoretical Computer Science 13, 45–60
McMillan, K.L.: Symbolic model checking. Kluwer Academic Publishers, Dordrecht (1993)
Burch, J.R., Clarke, E.M., McMillan, K.L.: Symbolic model checking: 1020 states and beyond. Information and Computation 98, 142–170 (1992)
Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers 35, 677–691 (1986)
Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999)
Jin, H., Somenzi, F.: An incremental algorithm to check satisfiability for bounded model checking. Electronic Notes in Theoretical Computer Science 119, 51–65 (2005)
Jin, H., Awedh, M., Somenzi, F.: CirCUs: A satisfiability solver geared towards bounded model checking. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 519–522. Springer, Heidelberg (2004)
Latvala, T., Biere, A., Heljanko, K., Junttila, T.: Simple is better: Efficient bounded model checking for past LTL. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 380–395. Springer, Heidelberg (2005)
Latvala, T., Biere, A., Heljanko, K., Junttila, T.: Simple bounded LTL model checking. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol. 3312, pp. 186–200. Springer, Heidelberg (2004)
Frisch, A., Sheridan, D., Walsh, T.: A fixpoint based encoding for bounded model checking. In: Aagaard, M.D., O’Leary, J.W. (eds.) FMCAD 2002. LNCS, vol. 2517, Springer, Heidelberg (2002)
Shtrichman, O.: Pruning techniques for the SAT-based Bounded Model Checking Problem. In: Margaria, T., Melham, T.F. (eds.) CHARME 2001. LNCS, vol. 2144, p. 58. Springer, Heidelberg (2001)
Shtrichman, O.: Tuning SAT checkers for Bounded Model-Checking. In: CAV. LNCS, vol. 1855 (2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Zhou, C., Ding, D. (2006). Improved SAT Based Bounded Model Checking. In: Cai, JY., Cooper, S.B., Li, A. (eds) Theory and Applications of Models of Computation. TAMC 2006. Lecture Notes in Computer Science, vol 3959. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11750321_58
Download citation
DOI: https://doi.org/10.1007/11750321_58
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-34021-8
Online ISBN: 978-3-540-34022-5
eBook Packages: Computer ScienceComputer Science (R0)