Top

Published in:

2015 | OriginalPaper | Chapter

Model Counting for Complex Data Structures

Authors : Antonio Filieri, Marcelo F. Frias, Corina S. Păsăreanu, Willem Visser

Published in: Model Checking Software

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter Symbolic Causality Checking Using Bounded Model Checking

next chapter Parallel SAT-Based Parameterised Three-Valued Model Checking

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) CrossRef

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)MATHMathSciNetCrossRef

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)MATHMathSciNet

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)MATHMathSciNetCrossRef

Boyapati, C., Khurshid, S., Marinov, D.: Korat: automated testing based on Java predicates. In: ISSTA, pp. 123–133 (2002)

10.

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)

11.

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)

12.

Clarke, L.A.: A system to generate test data and symbolically execute programs. IEEE Trans. Soft. Eng. 2(3), 215–222 (1976)CrossRef

13.

Cormen, T.H.: Introduction to Algorithms, 3rd edn. MIT Press, Cambridge (2009)MATH

14.

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)CrossRef

15.

Filieri, A., Pasareanu, C.S., Visser, W.: Reliability analysis in symbolic pathfinder. In: ICSE, pp. 622–631 (2013)

16.

Filieri, A., Pasareanu, C.S., Visser, W., Geldenhuys, J.: Statistical symbolic execution with informed sampling. In: FSE, pp. 437–448 (2014)

17.

Galeotti, J.P., Rosner, N., Pombo, CGL., Frias, M.F.: Analysis of invariants for efficient bounded verification. In: ISSTA, USA, pp. 25–36 (2010)

18.

Geldenhuys, J., Dwyer, M.B., Visser, W.: Probabilistic symbolic execution. In: ISSTA, pp. 166–176 (2012)

19.

Ghezzi, C., Pezzè, M., Sama, M., Tamburrelli, G.: Mining behavior models from user-intensive web applications. In: ICSE, pp. 277–287 (2014)

20.

Godefroid, P., Klarlund, N., Sen, K.: Dart: directed automated random testing. In: PLDI, pp. 213–223 (2005)

21.

Gordon, A.D., Henzinger, T.A., Nori, A.V., Rajamani, S.K.: Probabilistic programming. In: ICSE FOSE, pp. 167–181 (2014)

22.

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) CrossRef

23.

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)CrossRef

24.

Jackson, D.: Alloy: a lightweight object modelling notation. ACM Trans. Softw. Eng. Methodol. 11(2), 256–290 (2002)CrossRef

25.

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) CrossRef

26.

King, J.C.: Symbolic execution and program testing. Comm. ACM 19(7), 385–394 (1976)MATHMathSciNetCrossRef

27.

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)

28.

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)

29.

Luu, L., Shinde, S., Saxena, P., Demsky, B.: A model counter for constraints over unbounded strings. In: PLDI, p. 57 (2014)

30.

Monniaux, D.: An abstract Monte-Carlo method for the analysis of probabilistic programs. In: POPL, pp. 93–101 (2001)

31.

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

32.

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)CrossRef

33.

Pestman, W.R.: Mathematical Statistics. De Gruyter, Berlin (2009)MATHCrossRef

34.

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)

35.

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)

36.

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)

37.

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) CrossRef

38.

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)

39.

Visser, W., Pasareanu, C.S., Pelanek, R.: Test input generation for Java containers using state matching. In: ISSTA, pp. 37–48 (2006)

40.

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) CrossRef

41.

Zuliani, P., Platzer, A., Clarke, E.M.: Bayesian statistical model checking with application to Simulink/Stateflow verification. In: HSCC, pp. 243–252. ACM (2010)

Title: Model Counting for Complex Data Structures
Authors: Antonio Filieri
Marcelo F. Frias
Corina S. Păsăreanu
Willem Visser
Publisher: Springer International Publishing
Book: Model Checking Software
Print ISBN: 978-3-319-23403-8

Electronic ISBN: 978-3-319-23404-5

Copyright Year: 2015
DOI: https://doi.org/10.1007/978-3-319-23404-5_15

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner