Abstract
Bounded Model Checking (BMC) encodes a model checking problem in the propositional logic. Diagnosing the resulting formula to be satisfiable provides a counterexample. While surprisingly efficient for many complex systems, in general BMC still fails to be complete and is a method of falsification rather then validation. The major obstacle is satisfiability testing (SAT). The paper introduces a selective search to the standard DLL SAT algorithm, allowing to profit from several optimization techniques proposed for non-symbolic methods. Partial-order reductions are shown as an example of selective search. Preliminary experimental results confirm that the selective search can significantly improve the effectiveness of BMC.
Partly supported by the Ministry of Science and the Information Society Technologies under the grant No. 3T11C01128.
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
Alur, R., Brayton, R., Henzinger, T.A., Qadeer, S., Ramajani, S.: Partial order reduction in symbolic state-space exploration. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254. Springer, Heidelberg (1997)
Biere, A., Cimatti, A., Clarke, E., Strichman, O., Zhu, Y.: Bounded model checking. In: Highly Dependable Software, Advances in Computers, vol. 58. Academic Press, London (2003)
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)
Clarke, E., Grumberg, O., Minea, M., Peled, D.: State space reduction using partial order techniques. Software Tools for Technology Transfer 2(3), 279–287 (1999)
Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: Proc. of the 38th Design Automation Conference (DAC 2001) (June 2001)
Nabiałek, W., Niewiadomski, A., Penczek, W., Półrola, A., Szreter, M.: VerICS 2004: A model checker for real time and multi-agent systems. In: Proc. of the Int. Workshop on Concurrency, Specification and Programming (CS&P 2004), Informatik-Berichte, vol. 170(1), Humboldt University (2004)
Plaisted, D., Greenbaum, S.: A structure-preserving clause form translation. Journal of Symbolic Computation 2(3), 293–304 (1986)
Penczek, W., Woźna, B., Zbrzezny, A.: Towards bounded model checking for the universal fragment of TCTL. In: Damm, W., Olderog, E.-R. (eds.) FTRTFT 2002. LNCS, vol. 2469, p. 265. Springer, Heidelberg (2002)
Strichman, O.: Tuning SAT checkers for bounded model checking. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855. Springer, Heidelberg (2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Szreter, M. (2005). Selective Search in Bounded Model Checking of Reachability Properties. In: Peled, D.A., Tsay, YK. (eds) Automated Technology for Verification and Analysis. ATVA 2005. Lecture Notes in Computer Science, vol 3707. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11562948_14
Download citation
DOI: https://doi.org/10.1007/11562948_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-29209-8
Online ISBN: 978-3-540-31969-6
eBook Packages: Computer ScienceComputer Science (R0)