Abstract
In symbolic software model checking, most approaches use predicates as symbolic representation of the state space, and SMT solvers for computations on the state space; BDDs are sometimes used as auxiliary data structure. The representation of software state spaces by BDDs was not yet thoroughly investigated, although BDDs are successful in hardware verification. The reason for this is that BDDs do not efficiently support all operations that are needed in software verification. In this work, we evaluate the use of a pure BDD representation of integer variable values, and focus on a particular class of programs: event-conditionaction systems with limited operations. A symbolic representation using BDDs seems appropriate for this particular class of programs. We implement a program analysis based on BDDs and experimentally compare three symbolic techniques to verify reachability properties of ECA programs. The results show that BDDs are efficient, which yields the insight that BDDs could be used selectively for some variables (to be determined by a pre-analysis), even in general software model checking.
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
Berndl, M., Lhoták, O., Qian, F., Hendren, L., Umanee, N.: Points-to Analysis using BDDs. In: Proc. PLDI, pp. 103–114. ACM (2003)
Beyer, D.: Relational Programming with CrocoPat. In: Proc. ICSE, pp. 807–810. ACM (2006)
Beyer, D.: Competition on Software Verification (SV-COMP). In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 504–524. Springer, Heidelberg (2012)
Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: The Software Model Checker Blast. Int. J. Softw. Tools Technol. Transfer 9(5-6), 505–525 (2007)
Beyer, D., Henzinger, T.A., Théoduloz, G.: Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 504–518. Springer, Heidelberg (2007)
Beyer, D., Keremoglu, M.E.: CPAchecker: A Tool for Configurable Software Verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 184–190. Springer, Heidelberg (2011)
Beyer, D., Keremoglu, M.E., Wendler, P.: Predicate Abstraction with Adjustable-Block Encoding. In: Proc. FMCAD, pp. 189–197 (2010)
Beyer, D., Lewerentz, C., Noack, A.: Rabbit: A Tool for BDD-Based Verification of Real-Time Systems. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 122–125. Springer, Heidelberg (2003)
Beyer, D., Wendler, P.: Algorithms for Software Model Checking: Predicate Abstraction vs. IMPACT. In: Proc. FMCAD (2012)
Bryant, R.E.: Graph-Based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers C-35(8), 677–691 (1986)
Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L.: Sequential Circuit Verification using Symbolic Model Checking. In: Proc. DAC, pp. 46–51. ACM (1990)
Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic Model Checking: 1020 States and Beyond. In: Proc. LICS, pp. 428–439. IEEE (1990)
Campos, S.V.A., Clarke, E.M.: The Verus Language: Representing Time Efficiently with BDDs. In: Rus, T., Bertrán, M. (eds.) ARTS 1997. LNCS, vol. 1231, pp. 64–78. Springer, Heidelberg (1997)
Esparza, J., Kiefer, S., Schwoon, S.: Abstraction Refinement with Craig Interpolation and Symbolic Pushdown Systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 489–503. Springer, Heidelberg (2006)
Howar, F., Isberner, M., Merten, M., Steffen, B., Beyer, D.: The RERS Grey-Box Challenge 2012: Analysis of Event-Condition-Action Systems. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012, Part I. LNCS, vol. 7609, pp. 608–614. Springer, Heidelberg (2012)
McMillan, K.L.: The SMV System. Technical Report CMU-CS-92-131, Carnegie Mellon University (1992)
McMillan, K.L.: Lazy Abstraction with Interpolants. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 123–136. Springer, Heidelberg (2006)
Necula, G.C., McPeak, S., Rahul, S.P., Weimer, W.: CIL: Intermediate Language and Tools for Analysis and Transformation of C Programs. In: Horspool, R.N. (ed.) CC 2002. LNCS, vol. 2304, pp. 213–228. Springer, Heidelberg (2002)
von Rhein, A., Apel, S., Raimondi, F.: Introducing Binary Decision Diagrams in the Explicit-State Verification of Java Code. In: Proc. Java Pathfinder Workshop (2011)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Beyer, D., Stahlbauer, A. (2013). BDD-Based Software Model Checking with CPAchecker . In: Kučera, A., Henzinger, T.A., Nešetřil, J., Vojnar, T., Antoš, D. (eds) Mathematical and Engineering Methods in Computer Science. MEMICS 2012. Lecture Notes in Computer Science, vol 7721. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-36046-6_1
Download citation
DOI: https://doi.org/10.1007/978-3-642-36046-6_1
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-36044-2
Online ISBN: 978-3-642-36046-6
eBook Packages: Computer ScienceComputer Science (R0)