{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,30]],"date-time":"2025-05-30T05:10:01Z","timestamp":1748581801627,"version":"3.41.0"},"publisher-location":"Cham","reference-count":41,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319234038"},{"type":"electronic","value":"9783319234045"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-23404-5_15","type":"book-chapter","created":{"date-parts":[[2015,8,26]],"date-time":"2015-08-26T00:57:19Z","timestamp":1440550639000},"page":"222-241","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":15,"title":["Model Counting for Complex Data Structures"],"prefix":"10.1007","author":[{"given":"Antonio","family":"Filieri","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marcelo F.","family":"Frias","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Corina S.","family":"P\u0103s\u0103reanu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Willem","family":"Visser","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,8,27]]},"reference":[{"key":"15_CR1","unstructured":"RelSat tool. http:\/\/code.google.com\/p\/relsat\/"},{"key":"15_CR2","unstructured":"LattE (2013). https:\/\/www.math.ucdavis.edu\/~latte\/"},{"key":"15_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/978-3-642-54108-7_2","volume-title":"Verified Software: Theories, Tools, Experiments","author":"A Adje","year":"2014","unstructured":"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\u201347. Springer, Heidelberg (2014)"},{"issue":"4","key":"15_CR4","doi-asserted-by":"publisher","first-page":"769","DOI":"10.1287\/moor.19.4.769","volume":"19","author":"AI Barvinok","year":"1994","unstructured":"Barvinok, A.I.: A polynomial time algorithm for counting integral points in polyhedra when the dimension is fixed. Math. Oper. Res. 19(4), 769\u2013779 (1994)","journal-title":"Math. Oper. Res."},{"key":"15_CR5","doi-asserted-by":"crossref","unstructured":"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\u2013277 (2011)","DOI":"10.1145\/2025113.2025151"},{"key":"15_CR6","doi-asserted-by":"crossref","first-page":"457","DOI":"10.1613\/jair.601","volume":"10","author":"E Birnbaum","year":"1999","unstructured":"Birnbaum, E., Lozinskii, E.L.: The good old davis-putnam procedure helps counting models. J. Artif. Intell. Res. (JAIR) 10, 457\u2013477 (1999)","journal-title":"J. Artif. Intell. Res. (JAIR)"},{"key":"15_CR7","doi-asserted-by":"crossref","unstructured":"Borges, M., Filieri, A., d\u2019Amorim, M., P\u0103s\u0103reanu, C.S., Visser, W.: Compositional solution space quantification for probabilistic software analysis. In: PLDI, pp. 123\u2013132. ACM (2014)","DOI":"10.1145\/2666356.2594329"},{"key":"15_CR8","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/s00607-011-0182-8","volume":"94","author":"O Bouissou","year":"2012","unstructured":"Bouissou, O., Goubault, E., Goubault-Larrecq, J., Putot, S.: A generalization of p-boxes to affine arithmetic. Computing 94, 189\u2013201 (2012)","journal-title":"Computing"},{"key":"15_CR9","doi-asserted-by":"crossref","unstructured":"Boyapati, C., Khurshid, S., Marinov, D.: Korat: automated testing based on Java predicates. In: ISSTA, pp. 123\u2013133 (2002)","DOI":"10.1145\/566171.566191"},{"key":"15_CR10","unstructured":"Cadar, C., Dunbar, D., Engler, D.R.: Klee: unassisted and automatic generation of high-coverage tests for complex systems programs. In: OSDI, pp. 209\u2013224 (2008)"},{"key":"15_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"320","DOI":"10.1007\/978-3-662-46681-0_26","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"DV Chistikov","year":"2015","unstructured":"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\u2013334. Springer, Heidelberg (2015)"},{"issue":"3","key":"15_CR12","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1109\/TSE.1976.233817","volume":"2","author":"LA Clarke","year":"1976","unstructured":"Clarke, L.A.: A system to generate test data and symbolically execute programs. IEEE Trans. Soft. Eng. 2(3), 215\u2013222 (1976)","journal-title":"IEEE Trans. Soft. Eng."},{"key":"15_CR13","volume-title":"Introduction to Algorithms","author":"TH Cormen","year":"2009","unstructured":"Cormen, T.H.: Introduction to Algorithms, 3rd edn. MIT Press, Cambridge (2009)","edition":"3"},{"issue":"3\/4","key":"15_CR14","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1145\/2110170.2110175","volume":"45","author":"JA De Loera","year":"2012","unstructured":"De Loera, J.A., Dutra, B., K\u00f6ppe, M., Moreinis, S., Pinto, G., Wu, J.: Software for exact integration of polynomials over polyhedra. ACM Commun. Comput. Algebra 45(3\/4), 169\u2013172 (2012)","journal-title":"ACM Commun. Comput. Algebra"},{"key":"15_CR15","doi-asserted-by":"crossref","unstructured":"Filieri, A., Pasareanu, C.S., Visser, W.: Reliability analysis in symbolic pathfinder. In: ICSE, pp. 622\u2013631 (2013)","DOI":"10.1109\/ICSE.2013.6606608"},{"key":"15_CR16","doi-asserted-by":"crossref","unstructured":"Filieri, A., Pasareanu, C.S., Visser, W., Geldenhuys, J.: Statistical symbolic execution with informed sampling. In: FSE, pp. 437\u2013448 (2014)","DOI":"10.1145\/2635868.2635899"},{"key":"15_CR17","doi-asserted-by":"crossref","unstructured":"Galeotti, J.P., Rosner, N., Pombo, CGL., Frias, M.F.: Analysis of invariants for efficient bounded verification. In: ISSTA, USA, pp. 25\u201336 (2010)","DOI":"10.1145\/1831708.1831712"},{"key":"15_CR18","doi-asserted-by":"crossref","unstructured":"Geldenhuys, J., Dwyer, M.B., Visser, W.: Probabilistic symbolic execution. In: ISSTA, pp. 166\u2013176 (2012)","DOI":"10.1145\/2338965.2336773"},{"key":"15_CR19","doi-asserted-by":"crossref","unstructured":"Ghezzi, C., Pezz\u00e8, M., Sama, M., Tamburrelli, G.: Mining behavior models from user-intensive web applications. In: ICSE, pp. 277\u2013287 (2014)","DOI":"10.1145\/2568225.2568234"},{"key":"15_CR20","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Klarlund, N., Sen, K.: Dart: directed automated random testing. In: PLDI, pp. 213\u2013223 (2005)","DOI":"10.1145\/1064978.1065036"},{"key":"15_CR21","doi-asserted-by":"crossref","unstructured":"Gordon, A.D., Henzinger, T.A., Nori, A.V., Rajamani, S.K.: Probabilistic programming. In: ICSE FOSE, pp. 167\u2013181 (2014)","DOI":"10.1145\/2593882.2593900"},{"key":"15_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1007\/11691372_29","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Hinton","year":"2006","unstructured":"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\u2013444. Springer, Heidelberg (2006)"},{"issue":"9","key":"15_CR23","doi-asserted-by":"publisher","first-page":"1283","DOI":"10.1109\/TSE.2013.15","volume":"39","author":"J Galeotti","year":"2013","unstructured":"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\u20131307 (2013)","journal-title":"IEEE Trans. Soft. Eng."},{"issue":"2","key":"15_CR24","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1145\/505145.505149","volume":"11","author":"D Jackson","year":"2002","unstructured":"Jackson, D.: Alloy: a lightweight object modelling notation. ACM Trans. Softw. Eng. Methodol. 11(2), 256\u2013290 (2002)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"15_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"553","DOI":"10.1007\/3-540-36577-X_40","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Khurshid","year":"2003","unstructured":"Khurshid, S., P\u0103s\u0103reanu, 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\u2013568. Springer, Heidelberg (2003)"},{"issue":"7","key":"15_CR26","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1145\/360248.360252","volume":"19","author":"JC King","year":"1976","unstructured":"King, J.C.: Symbolic execution and program testing. Comm. ACM 19(7), 385\u2013394 (1976)","journal-title":"Comm. ACM"},{"key":"15_CR27","unstructured":"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\u2013102 (2003)"},{"key":"15_CR28","doi-asserted-by":"crossref","unstructured":"Luckow, K., P\u0103s\u0103reanu, C.S., Dwyer, M.B., Filieri, A., Visser, W.: Exact and approximate probabilistic symbolic execution for nondeterministic programs. In: ASE, pp. 575\u2013586. ACM (2014)","DOI":"10.1145\/2642937.2643011"},{"key":"15_CR29","doi-asserted-by":"crossref","unstructured":"Luu, L., Shinde, S., Saxena, P., Demsky, B.: A model counter for constraints over unbounded strings. In: PLDI, p. 57 (2014)","DOI":"10.1145\/2594291.2594331"},{"key":"15_CR30","doi-asserted-by":"crossref","unstructured":"Monniaux, D.: An abstract Monte-Carlo method for the analysis of probabilistic programs. In: POPL, pp. 93\u2013101 (2001)","DOI":"10.1145\/373243.360211"},{"key":"15_CR31","doi-asserted-by":"crossref","unstructured":"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","DOI":"10.1609\/aaai.v28i1.9060"},{"issue":"3","key":"15_CR32","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1007\/s10515-013-0122-2","volume":"20","author":"CS Pasareanu","year":"2013","unstructured":"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\u2013425 (2013)","journal-title":"Autom. Softw. Eng."},{"key":"15_CR33","doi-asserted-by":"publisher","DOI":"10.1515\/9783110208535","volume-title":"Mathematical Statistics","author":"WR Pestman","year":"2009","unstructured":"Pestman, W.R.: Mathematical Statistics. De Gruyter, Berlin (2009)"},{"key":"15_CR34","doi-asserted-by":"crossref","unstructured":"Phan, Q.-S., Malacaria, P., P\u0103s\u0103reanu, C.S., D\u2019Amorim, M.: Quantifying information leaks using reliability analysis. In: SPIN, pp. 105\u2013108. ACM (2014)","DOI":"10.1145\/2632362.2632367"},{"key":"15_CR35","first-page":"639","volume":"99","author":"N Rosner","year":"2015","unstructured":"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\u2013660 (2015)","journal-title":"IEEE Trans. Soft. Eng."},{"key":"15_CR36","doi-asserted-by":"crossref","unstructured":"Sankaranarayanan, S., Chakarov, A., Gulwani, S.: Static analysis for probabilistic programs: inferring whole program properties from finitely many paths. In: PLDI, pp. 447\u2013458 (2013)","DOI":"10.1145\/2499370.2462179"},{"key":"15_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/978-3-540-79124-9_10","volume-title":"Tests and Proofs","author":"N Tillmann","year":"2008","unstructured":"Tillmann, N., de Halleux, J.: Pex-white box test generation for NET. In: Beckert, B., H\u00e4hnle, R. (eds.) TAP 2008. LNCS, vol. 4966, pp. 134\u2013153. Springer, Heidelberg (2008)"},{"key":"15_CR38","doi-asserted-by":"crossref","unstructured":"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\u201328 (2002)","DOI":"10.1109\/ASAP.2002.1030701"},{"key":"15_CR39","doi-asserted-by":"crossref","unstructured":"Visser, W., Pasareanu, C.S., Pelanek, R.: Test input generation for Java containers using state matching. In: ISSTA, pp. 37\u201348 (2006)","DOI":"10.1145\/1146238.1146243"},{"key":"15_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"530","DOI":"10.1007\/978-3-540-24730-2_39","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G Yorsh","year":"2004","unstructured":"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\u2013545. Springer, Heidelberg (2004)"},{"key":"15_CR41","doi-asserted-by":"crossref","unstructured":"Zuliani, P., Platzer, A., Clarke, E.M.: Bayesian statistical model checking with application to Simulink\/Stateflow verification. In: HSCC, pp. 243\u2013252. ACM (2010)","DOI":"10.21236\/ADA531406"}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-23404-5_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,30]],"date-time":"2025-05-30T04:38:02Z","timestamp":1748579882000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-23404-5_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319234038","9783319234045"],"references-count":41,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-23404-5_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"27 August 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}