Abstract
We present algorithms to efficiently bound the depth of the state spaces explored by explicit-state model checkers. Given a parameter k, our algorithms guarantee finding any violation of an invariant that is witnessed using a counterexample of length k or less from the initial state. Though depth bounding is natural with breadth-first search, explicit-state model checkers are unable to use breadth first search due to prohibitive space requirements, and use depth-first search to explore large state spaces. Thus, we explore efficient ways to perform depth bounding with depth-first search. We prove our algorithms sound (in the sense that they explore exactly all the states reachable within a depth bound), and show their effectiveness on large real-life models from Microsoft’s product groups.
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
Andrews, T., Qadeer, S., Rajamani, S.K., Rehof, J., Xie, Y.: Zing: A model checker for concurrent software. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 484–487. Springer, Heidelberg (2004)
Andrews, T., Qadeer, S., Rajamani, S.K., Rehof, J., Xie, Y.: Zing: Exploiting program structure for model checking concurrent software. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 1–15. Springer, Heidelberg (2004)
Ball, T., Rajamani, S.K.: The SLAM Project: Debugging system software via static analysis. In: POPL 2002: Principles of Programming Languages, pp. 1–3. ACM, New York (2002)
Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 1020 states and beyond. In: LICS 1990: Logic in Computer Science, pp. 428–439 (1990)
Clarke, E.M., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Formal Methods in System Design 19(1), 7–34 (2001)
Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154–169. Springer, Heidelberg (2000)
Courcoubetis, C., Vardi, M.Y., Wolper, P., Yannakakis, M.: Memory efficient algorithms for the verification of temporal properties. In: Clarke, E., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol. 531, pp. 58–328. Springer, Heidelberg (1991)
Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem. Springer, Heidelberg (1996)
Godefroid, P.: Software Model Checking: The Verisoft Approach. Formal Methods in System Design 26, 77–101 (2005)
Havelund, K., Pressburger, T.: Model checking Java programs using Java PathFinder. International Journal on Software Tools for Technology Transfer (STTT) 2, 366–381 (2000)
Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: POPL 2002: Principles of Programming Languages, pp. 58–70. ACM, New York (2002)
Holzmann, G.: The model checker SPIN. IEEE Transactions on Software Engineering 23(5), 279–295 (May 1997)
Holzmann, G.J.: An analysis of bitstate hashing. Form. Methods Syst. Des. 13, 289–307 (1998)
Jackson, D.: Software Abstractions: Logic, Language, and Analysis. MIT Press, Cambridge (2006)
Katz, S., Peled, D.: Verification of distributed programs using representative interleaving sequences, vol. 6, pp. 107–120 (1992)
Korf, R.E.: Depth-first Iterative-deepening: An Optimal Admissible Tree Search. In the Journal of Artificial Intelligence 27, 97–109 (1985)
Musuvathi, M., Park, D.Y.W., Chou, A., Engler, D.R., Dill, D.L.: CMC: a pragmatic approach to model checking real code. SIGOPS Oper. Syst. Rev. 36, 75–88 (2002)
Sistla, A.P., Godefroid, P.: Symmetry and reduced symmetry in model checking. ACM Trans. Program. Lang. Syst. 26, 702–734 (2004)
Stern, U., Dill, D.L.: Improved probabilistic verification by hash compaction. In: Camurati, P.E., Eveking, H. (eds.) CHARME 1995. LNCS, vol. 987, pp. 206–224. Springer, Heidelberg (1995)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Udupa, A., Desai, A., Rajamani, S. (2011). Depth Bounded Explicit-State Model Checking. In: Groce, A., Musuvathi, M. (eds) Model Checking Software. SPIN 2011. Lecture Notes in Computer Science, vol 6823. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-22306-8_5
Download citation
DOI: https://doi.org/10.1007/978-3-642-22306-8_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-22305-1
Online ISBN: 978-3-642-22306-8
eBook Packages: Computer ScienceComputer Science (R0)