Abstract
We extend recent approaches for calculating the probability of program behaviors, to allow model counting for complex data structures with numeric fields. We use symbolic execution with lazy initialization to compute the input structures leading to the occurrence of a target event, while keeping a symbolic representation of the constraints on the numeric data. Off-the-shelf model counting tools are used to count the solutions for numerical constraints and field bounds encoding data structure invariants are used to reduce the search space. The technique is implemented in the Symbolic PathFinder tool and evaluated on several complex data structures. Results show that the technique is much faster than an enumeration-based method that uses the Korat tool and also highlight the benefits of using the field bounds to speed up the analysis.
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
Similar content being viewed by others
References
RelSat tool. http://code.google.com/p/relsat/
LattE (2013). https://www.math.ucdavis.edu/~latte/
Adje, A., Bouissou, O., Goubault-Larrecq, J., Goubault, E., Putot, S.: Static analysis of programs with imprecise probabilistic inputs. In: Cohen, E., Rybalchenko, A. (eds.) VSTTE 2013. LNCS, vol. 8164, pp. 22–47. Springer, Heidelberg (2014)
Barvinok, A.I.: A polynomial time algorithm for counting integral points in polyhedra when the dimension is fixed. Math. Oper. Res. 19(4), 769–779 (1994)
Beschastnikh, I., Brun, Y., Schneider, S., Sloan, M., Ernst, M.D.: Leveraging existing instrumentation to automatically infer invariant-constrained models. In: ESEC/FSE, pp. 267–277 (2011)
Birnbaum, E., Lozinskii, E.L.: The good old davis-putnam procedure helps counting models. J. Artif. Intell. Res. (JAIR) 10, 457–477 (1999)
Borges, M., Filieri, A., d’Amorim, M., Păsăreanu, C.S., Visser, W.: Compositional solution space quantification for probabilistic software analysis. In: PLDI, pp. 123–132. ACM (2014)
Bouissou, O., Goubault, E., Goubault-Larrecq, J., Putot, S.: A generalization of p-boxes to affine arithmetic. Computing 94, 189–201 (2012)
Boyapati, C., Khurshid, S., Marinov, D.: Korat: automated testing based on Java predicates. In: ISSTA, pp. 123–133 (2002)
Cadar, C., Dunbar, D., Engler, D.R.: Klee: unassisted and automatic generation of high-coverage tests for complex systems programs. In: OSDI, pp. 209–224 (2008)
Chistikov, D.V., Dimitrova, R., Majumdar, R.: Approximate counting in SMT and value estimation for probabilistic programs. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 320–334. Springer, Heidelberg (2015)
Clarke, L.A.: A system to generate test data and symbolically execute programs. IEEE Trans. Soft. Eng. 2(3), 215–222 (1976)
Cormen, T.H.: Introduction to Algorithms, 3rd edn. MIT Press, Cambridge (2009)
De Loera, J.A., Dutra, B., Köppe, M., Moreinis, S., Pinto, G., Wu, J.: Software for exact integration of polynomials over polyhedra. ACM Commun. Comput. Algebra 45(3/4), 169–172 (2012)
Filieri, A., Pasareanu, C.S., Visser, W.: Reliability analysis in symbolic pathfinder. In: ICSE, pp. 622–631 (2013)
Filieri, A., Pasareanu, C.S., Visser, W., Geldenhuys, J.: Statistical symbolic execution with informed sampling. In: FSE, pp. 437–448 (2014)
Galeotti, J.P., Rosner, N., Pombo, CGL., Frias, M.F.: Analysis of invariants for efficient bounded verification. In: ISSTA, USA, pp. 25–36 (2010)
Geldenhuys, J., Dwyer, M.B., Visser, W.: Probabilistic symbolic execution. In: ISSTA, pp. 166–176 (2012)
Ghezzi, C., Pezzè, M., Sama, M., Tamburrelli, G.: Mining behavior models from user-intensive web applications. In: ICSE, pp. 277–287 (2014)
Godefroid, P., Klarlund, N., Sen, K.: Dart: directed automated random testing. In: PLDI, pp. 213–223 (2005)
Gordon, A.D., Henzinger, T.A., Nori, A.V., Rajamani, S.K.: Probabilistic programming. In: ICSE FOSE, pp. 167–181 (2014)
Hinton, A., Kwiatkowska, M., Norman, G., Parker, D.: PRISM: a tool for automatic verification of probabilistic systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 441–444. Springer, Heidelberg (2006)
Galeotti, J., Rosner, N., Lopez Pombo, C., Frias, M.F.: Taco: efficient sat-based bounded verification using symmetry breaking and tight bounds. IEEE Trans. Soft. Eng. 39(9), 1283–1307 (2013)
Jackson, D.: Alloy: a lightweight object modelling notation. ACM Trans. Softw. Eng. Methodol. 11(2), 256–290 (2002)
Khurshid, S., Păsăreanu, C.S., Visser, W.: Generalized symbolic execution for model checking and testing. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 553–568. Springer, Heidelberg (2003)
King, J.C.: Symbolic execution and program testing. Comm. ACM 19(7), 385–394 (1976)
Lisper, B.: Fully automatic, parametric worst-case execution time analysis. In: Proceedings of the 3rd International Workshop on Worst-Case Execution Time Analysis, WCET, pp. 99–102 (2003)
Luckow, K., Păsăreanu, C.S., Dwyer, M.B., Filieri, A., Visser, W.: Exact and approximate probabilistic symbolic execution for nondeterministic programs. In: ASE, pp. 575–586. ACM (2014)
Luu, L., Shinde, S., Saxena, P., Demsky, B.: A model counter for constraints over unbounded strings. In: PLDI, p. 57 (2014)
Monniaux, D.: An abstract Monte-Carlo method for the analysis of probabilistic programs. In: POPL, pp. 93–101 (2001)
Nori, A.V., Hur, C.-K., Rajamani, S.K., Samuel, S.: R2: an efficient mcmc sampler for probabilistic programs. In: AAAI Conference on Artificial Intelligence (AAAI). AAAI, July 2014
Pasareanu, C.S., Visser, W., Bushnell, D.H., Geldenhuys, J., Mehlitz, P.C., Rungta, N.: Symbolic pathfinder: integrating symbolic execution with model checking for Java bytecode analysis. Autom. Softw. Eng. 20(3), 391–425 (2013)
Pestman, W.R.: Mathematical Statistics. De Gruyter, Berlin (2009)
Phan, Q.-S., Malacaria, P., Păsăreanu, C.S., D’Amorim, M.: Quantifying information leaks using reliability analysis. In: SPIN, pp. 105–108. ACM (2014)
Rosner, N., Geldenhuys, J., Aguirre, N., Visser, W., Frias, M.F.: Bliss: improved symbolic execution by bounded lazy initialization with sat support. IEEE Trans. Soft. Eng. 99, 639–660 (2015)
Sankaranarayanan, S., Chakarov, A., Gulwani, S.: Static analysis for probabilistic programs: inferring whole program properties from finitely many paths. In: PLDI, pp. 447–458 (2013)
Tillmann, N., de Halleux, J.: Pex-white box test generation for NET. In: Beckert, B., Hähnle, R. (eds.) TAP 2008. LNCS, vol. 4966, pp. 134–153. Springer, Heidelberg (2008)
Turjan, A., Kienhuis, B., Deprettere, E.F.: A compile time based approach for solving out-of-order communication in Kahn process networks. In: ASAP, pp. 17–28 (2002)
Visser, W., Pasareanu, C.S., Pelanek, R.: Test input generation for Java containers using state matching. In: ISSTA, pp. 37–48 (2006)
Yorsh, G., Reps, T.W., Sagiv, M.: Symbolically computing most-precise abstract operations for shape analysis. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 530–545. Springer, Heidelberg (2004)
Zuliani, P., Platzer, A., Clarke, E.M.: Bayesian statistical model checking with application to Simulink/Stateflow verification. In: HSCC, pp. 243–252. ACM (2010)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Filieri, A., Frias, M.F., Păsăreanu, C.S., Visser, W. (2015). Model Counting for Complex Data Structures. In: Fischer, B., Geldenhuys, J. (eds) Model Checking Software. SPIN 2015. Lecture Notes in Computer Science(), vol 9232. Springer, Cham. https://doi.org/10.1007/978-3-319-23404-5_15
Download citation
DOI: https://doi.org/10.1007/978-3-319-23404-5_15
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-23403-8
Online ISBN: 978-3-319-23404-5
eBook Packages: Computer ScienceComputer Science (R0)