{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T17:25:36Z","timestamp":1725902736284},"publisher-location":"Cham","reference-count":87,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319600734"},{"type":"electronic","value":"9783319600741"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-60074-1_1","type":"book-chapter","created":{"date-parts":[[2017,6,28]],"date-time":"2017-06-28T13:37:38Z","timestamp":1498657058000},"page":"1-25","source":"Crossref","is-referenced-by-count":2,"title":["Probabilistic Program Analysis"],"prefix":"10.1007","author":[{"given":"Matthew B.","family":"Dwyer","sequence":"first","affiliation":[]},{"given":"Antonio","family":"Filieri","sequence":"additional","affiliation":[]},{"given":"Jaco","family":"Geldenhuys","sequence":"additional","affiliation":[]},{"given":"Mitchell","family":"Gerrard","sequence":"additional","affiliation":[]},{"given":"Corina S.","family":"P\u0103s\u0103reanu","sequence":"additional","affiliation":[]},{"given":"Willem","family":"Visser","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,6,29]]},"reference":[{"key":"1_CR1","doi-asserted-by":"crossref","unstructured":"Aydin, A., Bang, L., Bultan, T.: Automata-based model counting for string constraints. In: Proceedings of the 27th International Conference on Computer Aided Verification, CAV 2015, Part I, San Francisco, CA, USA, 18\u201324 July 2015, pp. 255\u2013272 (2015)","DOI":"10.1007\/978-3-319-21690-4_15"},{"issue":"1","key":"1_CR2","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/j.scico.2007.08.001","volume":"72","author":"R Bagnara","year":"2008","unstructured":"Bagnara, R., Hill, P.M., Zaffanella, E.: The parma polyhedra library: toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Sci. Comput. Program. 72(1), 3\u201321 (2008)","journal-title":"Sci. Comput. Program."},{"key":"1_CR3","doi-asserted-by":"crossref","unstructured":"Bang, L., Aydin, A., Phan, Q., Pasareanu, C.S., Bultan, T.: String analysis for side channels with segmented oracles. In: Proceedings of the 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering, FSE 2016, Seattle, WA, USA, 13\u201318 November 2016, pp. 193\u2013204 (2016)","DOI":"10.1145\/2950290.2950362"},{"issue":"4","key":"1_CR4","doi-asserted-by":"crossref","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":"1_CR5","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-540-77974-2","volume-title":"Computational Geometry: Algorithms and Applications","author":"M Berg de","year":"2008","unstructured":"de Berg, M.: Computational Geometry: Algorithms and Applications. Springer, Heidelberg (2008)"},{"key":"1_CR6","series-title":"Frontiers in Artificial Intelligence and Applications","volume-title":"Handbook of Satisfiability","author":"A Biere","year":"2009","unstructured":"Biere, A., van Maaren, H.: Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications. IOS Press, Amsterdam (2009)"},{"key":"1_CR7","series-title":"Information Science and Statistics","volume-title":"Pattern Recognition and Machine Learning","author":"C Bishop","year":"2006","unstructured":"Bishop, C.: Pattern Recognition and Machine Learning. Information Science and Statistics. Springer, New York (2006)"},{"key":"1_CR8","doi-asserted-by":"crossref","unstructured":"Borges, M., Filieri, A., d\u2019Amorim, M., P\u0103s\u0103reanu, C.S.: Iterative distribution-aware sampling for probabilistic symbolic execution. In: Proceedings of the 10th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, ESEC\/FSE 2015. ACM (2015)","DOI":"10.1145\/2786805.2786832"},{"key":"1_CR9","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: Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 123\u2013132. ACM (2014)","DOI":"10.1145\/2666356.2594329"},{"issue":"3","key":"1_CR10","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1145\/136035.136043","volume":"24","author":"RE Bryant","year":"1992","unstructured":"Bryant, R.E.: Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Comput. Surv. (CSUR) 24(3), 293\u2013318 (1992)","journal-title":"ACM Comput. Surv. (CSUR)"},{"key":"1_CR11","unstructured":"Cadar, C., Dunbar, D., Engler, D.R.: Klee: Unassisted and automatic generation of high-coverage tests for complex systems programs. In: OSDI, vol. 8, pp. 209\u2013224 (2008)"},{"key":"1_CR12","doi-asserted-by":"crossref","unstructured":"Chakraborty, S., Fremont, D.J., Meel, K.S., Seshia, S.A., Vardi, M.Y.: Distribution-aware sampling and weighted model counting for SAT. In: Twenty-Eighth AAAI Conference on Artificial Intelligence (2014)","DOI":"10.1609\/aaai.v28i1.8990"},{"key":"1_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/978-3-642-40627-0_18","volume-title":"Principles and Practice of Constraint Programming","author":"S Chakraborty","year":"2013","unstructured":"Chakraborty, S., Meel, K.S., Vardi, M.Y.: A scalable approximate model counter. In: Schulte, C. (ed.) CP 2013. LNCS, vol. 8124, pp. 200\u2013216. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-40627-0_18"},{"key":"1_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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":"D Chistikov","year":"2015","unstructured":"Chistikov, D., 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). doi: 10.1007\/978-3-662-46681-0_26"},{"key":"1_CR15","doi-asserted-by":"crossref","unstructured":"Claret, G., Rajamani, S.K., Nori, A.V., Gordon, A.D., Borgstr\u00f6m, J.: Bayesian inference using data flow analysis. In: Proceedings of the 2013 9th Joint Meeting on Foundations of Software Engineering, pp. 92\u2013102. ACM (2013)","DOI":"10.1145\/2491411.2491423"},{"key":"1_CR16","volume-title":"Model Checking","author":"EM Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"1_CR17","doi-asserted-by":"crossref","first-page":"215","DOI":"10.1109\/TSE.1976.233817","volume":"3","author":"L Clarke","year":"1976","unstructured":"Clarke, L., et al.: A system to generate test data and symbolically execute programs. IEEE Trans. Software Eng. 3, 215\u2013222 (1976)","journal-title":"IEEE Trans. Software Eng."},{"key":"1_CR18","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp. 238\u2013252. ACM (1977)","DOI":"10.1145\/512950.512973"},{"key":"1_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/978-3-642-28869-2_9","volume-title":"Programming Languages and Systems","author":"P Cousot","year":"2012","unstructured":"Cousot, P., Monerau, M.: Probabilistic abstract interpretation. In: Seidl, H. (ed.) ESOP 2012. LNCS, vol. 7211, pp. 169\u2013193. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-28869-2_9"},{"key":"1_CR20","doi-asserted-by":"crossref","unstructured":"Di Pierro, A., Wiklicky, H.: Probabilistic data flow analysis: a linear equational approach. arXiv preprint arXiv:1307.4474 (2013)","DOI":"10.4204\/EPTCS.119.14"},{"key":"1_CR21","doi-asserted-by":"crossref","unstructured":"Dwyer, M.B.: Unifying testing and analysis through behavioral coverage. In: 2011 26th IEEE\/ACM International Conference on Automated Software Engineering (ASE), p. 2. IEEE (2011)","DOI":"10.1109\/ASE.2011.6100066"},{"key":"1_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"334","DOI":"10.1007\/978-3-642-23702-7_25","volume-title":"Static Analysis","author":"J Esparza","year":"2011","unstructured":"Esparza, J., Gaiser, A.: Probabilistic abstractions with arbitrary domains. In: Yahav, E. (ed.) SAS 2011. LNCS, vol. 6887, pp. 334\u2013350. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-23702-7_25"},{"key":"1_CR23","doi-asserted-by":"crossref","unstructured":"Filieri, A., Frias, M., P\u0103s\u0103reanu, C., Visser, W.: Model counting for complex data structures. In: Proceedings of the 2015 International SPIN Symposium on Model Checking of Software. ACM (2015)","DOI":"10.1007\/978-3-319-23404-5_15"},{"key":"1_CR24","doi-asserted-by":"crossref","unstructured":"Filieri, A., P\u0103s\u0103reanu, C.S., Visser, W., Geldenhuys, J.: Statistical symbolic execution with informed sampling. In: Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering, pp. 437\u2013448. ACM (2014)","DOI":"10.1145\/2635868.2635899"},{"key":"1_CR25","doi-asserted-by":"crossref","unstructured":"Filieri, A., P\u0103s\u0103reanu, C.S., Yang, G.: Quantification of software changes through probabilistic symbolic execution. In: Proceedings of the 30th IEEE\/ACM International Conference on Automated Software Engineering (ASE) - Short Paper, November 2015","DOI":"10.1109\/ASE.2015.78"},{"key":"1_CR26","doi-asserted-by":"crossref","unstructured":"Filieri, A., P\u0103s\u0103reanu, C.S., Visser, W.: Reliability analysis in symbolic pathfinder. In: Proceedings of the 2013 International Conference on Software Engineering, pp. 622\u2013631. IEEE Press (2013)","DOI":"10.1109\/ICSE.2013.6606608"},{"key":"1_CR27","unstructured":"Fink, S., Dolby, J.: WALA-The TJ watson libraries for analysis (2012)"},{"key":"1_CR28","doi-asserted-by":"crossref","unstructured":"Floyd, R.W.: Assigning meanings to programs. In: Mathematical Aspects of Computer Science, pp. 19\u201332 (1967)","DOI":"10.1090\/psapm\/019\/0235771"},{"issue":"3","key":"1_CR29","doi-asserted-by":"crossref","first-page":"305","DOI":"10.1145\/356674.356676","volume":"8","author":"LD Fosdick","year":"1976","unstructured":"Fosdick, L.D., Osterweil, L.J.: Data flow analysis in software reliability. ACM Comput. Surv. (CSUR) 8(3), 305\u2013330 (1976)","journal-title":"ACM Comput. Surv. (CSUR)"},{"issue":"2","key":"1_CR30","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1007\/BF00995736","volume":"1","author":"K Fu","year":"1972","unstructured":"Fu, K., Huang, T.: Stochastic grammars and languages. Int. J. Comput. Inform. Sci. 1(2), 135\u2013170 (1972)","journal-title":"Int. J. Comput. Inform. Sci."},{"key":"1_CR31","doi-asserted-by":"crossref","unstructured":"Geldenhuys, J., Dwyer, M.B., Visser, W.: Probabilistic symbolic execution. In: Proceedings of the 2012 International Symposium on Software Testing and Analysis, pp. 166\u2013176. ACM (2012)","DOI":"10.1145\/2338965.2336773"},{"key":"1_CR32","doi-asserted-by":"crossref","unstructured":"Gelman, A., Carlin, J., Stern, H., Dunson, D., Vehtari, A., Rubin, D.: Bayesian Data Analysis, 3rd edn. Chapman & Hall\/CRC Texts in Statistical Science, Taylor & Francis (2013)","DOI":"10.1201\/b16018"},{"key":"1_CR33","series-title":"Statistics and Computing","volume-title":"Random Number Generation and Monte Carlo Methods","author":"J Gentle","year":"2013","unstructured":"Gentle, J.: Random Number Generation and Monte Carlo Methods. Statistics and Computing. Springer, New York (2013)"},{"key":"1_CR34","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Klarlund, N., Sen, K.: DART: directed automated random testing. In: ACM Sigplan Notices, vol. 40, pp. 213\u2013223. ACM (2005)","DOI":"10.1145\/1065010.1065036"},{"key":"1_CR35","doi-asserted-by":"crossref","unstructured":"Gordon, A.D., Henzinger, T.A., Nori, A.V., Rajamani, S.K.: Probabilistic programming. In: Proceedings of the on Future of Software Engineering, pp. 167\u2013181. ACM (2014)","DOI":"10.1145\/2593882.2593900"},{"key":"1_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer Aided Verification","author":"S Graf","year":"1997","unstructured":"Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72\u201383. Springer, Heidelberg (1997). doi: 10.1007\/3-540-63166-6_10"},{"key":"1_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1007\/978-3-642-12002-2_30","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"EM Hahn","year":"2010","unstructured":"Hahn, E.M., Hermanns, H., Wachter, B., Zhang, L.: PASS: abstraction refinement for infinite probabilistic models. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 353\u2013357. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-12002-2_30"},{"issue":"1","key":"1_CR38","doi-asserted-by":"crossref","first-page":"47","DOI":"10.1016\/j.entcs.2006.06.004","volume":"164","author":"I Hasuo","year":"2006","unstructured":"Hasuo, I., Jacobs, B., Sokolova, A.: Generic trace theory. Electron. Notes Theor. Comput. Sci. 164(1), 47\u201365 (2006)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"1_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/978-3-540-24622-0_8","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"T H\u00e9rault","year":"2004","unstructured":"H\u00e9rault, T., Lassaigne, R., Magniette, F., Peyronnet, S.: Approximate probabilistic model checking. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 73\u201384. Springer, Heidelberg (2004). doi: 10.1007\/978-3-540-24622-0_8"},{"issue":"301","key":"1_CR40","doi-asserted-by":"crossref","first-page":"13","DOI":"10.1080\/01621459.1963.10500830","volume":"58","author":"W Hoeffding","year":"1963","unstructured":"Hoeffding, W.: Probability inequalities for sums of bounded random variables. J. Am. Stat. Assoc. 58(301), 13\u201330 (1963)","journal-title":"J. Am. Stat. Assoc."},{"key":"1_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1007\/978-3-642-38916-0_9","volume-title":"Tests and Proofs","author":"K Jamrozik","year":"2013","unstructured":"Jamrozik, K., Fraser, G., Tillman, N., Halleux, J.: Generating test suites with augmented dynamic symbolic execution. In: Veanes, M., Vigan\u00f2, L. (eds.) TAP 2013. LNCS, vol. 7942, pp. 152\u2013167. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-38916-0_9"},{"key":"1_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1007\/978-3-642-31424-7_26","volume-title":"Computer Aided Verification","author":"C Jegourel","year":"2012","unstructured":"Jegourel, C., Legay, A., Sedwards, S.: Cross-entropy optimisation of importance sampling parameters for statistical model checking. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 327\u2013342. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-31424-7_26"},{"key":"1_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1007\/978-3-642-39799-8_38","volume-title":"Computer Aided Verification","author":"C Jegourel","year":"2013","unstructured":"Jegourel, C., Legay, A., Sedwards, S.: Importance splitting for statistical model checking rare properties. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 576\u2013591. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-39799-8_38"},{"key":"1_CR44","doi-asserted-by":"crossref","unstructured":"Jones, C.: Probabilistic non-determinism (1990)","DOI":"10.1086\/psaprocbienmeetp.1990.2.193096"},{"key":"1_CR45","doi-asserted-by":"crossref","unstructured":"Kildall, G.A.: A unified approach to global program optimization. In: Proceedings of the 1st Annual ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp. 194\u2013206. ACM (1973)","DOI":"10.1145\/512927.512945"},{"issue":"7","key":"1_CR46","doi-asserted-by":"crossref","first-page":"385","DOI":"10.1145\/360248.360252","volume":"19","author":"JC King","year":"1976","unstructured":"King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385\u2013394 (1976)","journal-title":"Commun. ACM"},{"issue":"3","key":"1_CR47","doi-asserted-by":"crossref","first-page":"328","DOI":"10.1016\/0022-0000(81)90036-2","volume":"22","author":"D Kozen","year":"1981","unstructured":"Kozen, D.: Semantics of probabilistic programs. J. Comput. Syst. Sci. 22(3), 328\u2013350 (1981)","journal-title":"J. Comput. Syst. Sci."},{"key":"1_CR48","doi-asserted-by":"crossref","unstructured":"Kozen, D.: A probabilistic PDL. In: Proceedings of the Fifteenth Annual ACM Symposium on Theory of Computing, pp. 291\u2013297. ACM (1983)","DOI":"10.1145\/800061.808758"},{"key":"1_CR49","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Advances and challenges of probabilistic model checking. In: 2010 Proceedings of the 48th Annual Allerton Conference on Communication, Control, and Computing (Allerton) (2010)","DOI":"10.1109\/ALLERTON.2010.5707120"},{"key":"1_CR50","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"M Kwiatkowska","year":"2011","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585\u2013591. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-22110-1_47"},{"key":"1_CR51","unstructured":"Lam, P., Bodden, E., Lhot\u00e1k, O., Hendren, L.: The Soot framework for Java program analysis: a retrospective. In: Cetus Users and Compiler Infrastructure Workshop, Galveston Island, TX, October 2011"},{"key":"1_CR52","doi-asserted-by":"crossref","unstructured":"Lattner, C., Adve, V.: LLVM: a compilation framework for lifelong program analysis & transformation. In: Proceedings of the International Symposium on Code Generation and Optimization: Feedback-Directed and Runtime Optimization (2004)","DOI":"10.1109\/CGO.2004.1281665"},{"key":"1_CR53","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/978-3-642-16612-9_11","volume-title":"Runtime Verification","author":"A Legay","year":"2010","unstructured":"Legay, A., Delahaye, B., Bensalem, S.: Statistical model checking: an overview. In: Barringer, H., Falcone, Y., Finkbeiner, B., Havelund, K., Lee, I., Pace, G., Ro\u015fu, G., Sokolsky, O., Tillmann, N. (eds.) RV 2010. LNCS, vol. 6418, pp. 122\u2013135. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-16612-9_11"},{"key":"1_CR54","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: Proceedings of the 29th ACM\/IEEE International Conference on Automated Software Engineering, pp. 575\u2013586. ACM (2014)","DOI":"10.1145\/2642937.2643011"},{"key":"1_CR55","doi-asserted-by":"crossref","unstructured":"Luu, L., Shinde, S., Saxena, P., Demsky, B.: A model counter for constraints over unbounded strings. In: Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 565\u2013576. ACM (2014)","DOI":"10.1145\/2666356.2594331"},{"issue":"4","key":"1_CR56","doi-asserted-by":"crossref","first-page":"463","DOI":"10.3233\/JCS-130469","volume":"21","author":"P Mardziel","year":"2013","unstructured":"Mardziel, P., Magill, S., Hicks, M., Srivatsa, M.: Dynamic enforcement of knowledge-based security policies using probabilistic abstract interpretation. J. Comput. Secur. 21(4), 463\u2013532 (2013)","journal-title":"J. Comput. Secur."},{"key":"1_CR57","doi-asserted-by":"crossref","first-page":"647","DOI":"10.2307\/1913469","volume":"52","author":"JB McDonald","year":"1984","unstructured":"McDonald, J.B.: Some generalized functions for the size distribution of income. Econometrica J. Econometric Soc. 52, 647\u2013663 (1984)","journal-title":"Econometrica J. Econometric Soc."},{"key":"1_CR58","unstructured":"Meel, K.S.: Sampling techniques for boolean satisfiability. CoRR abs\/1404.6682 (2014). http:\/\/arxiv.org\/abs\/1404.6682"},{"key":"1_CR59","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"322","DOI":"10.1007\/978-3-540-45099-3_17","volume-title":"Static Analysis","author":"D Monniaux","year":"2000","unstructured":"Monniaux, D.: Abstract interpretation of probabilistic semantics. In: Palsberg, J. (ed.) SAS 2000. LNCS, vol. 1824, pp. 322\u2013339. Springer, Heidelberg (2000). doi: 10.1007\/978-3-540-45099-3_17"},{"key":"1_CR60","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1007\/3-540-45309-1_24","volume-title":"Programming Languages and Systems","author":"D Monniaux","year":"2001","unstructured":"Monniaux, D.: Backwards Abstract Interpretation of Probabilistic Programs. In: Sands, D. (ed.) ESOP 2001. LNCS, vol. 2028, pp. 367\u2013382. Springer, Heidelberg (2001). doi: 10.1007\/3-540-45309-1_24"},{"issue":"1","key":"1_CR61","doi-asserted-by":"crossref","first-page":"179","DOI":"10.1016\/j.scico.2005.02.008","volume":"58","author":"D Monniaux","year":"2005","unstructured":"Monniaux, D.: Abstract interpretation of programs as markov decision processes. Sci. Comput. Program. 58(1), 179\u2013205 (2005)","journal-title":"Sci. Comput. Program."},{"issue":"3","key":"1_CR62","doi-asserted-by":"crossref","first-page":"325","DOI":"10.1145\/229542.229547","volume":"18","author":"C Morgan","year":"1996","unstructured":"Morgan, C., McIver, A., Seidel, K.: Probabilistic predicate transformers. ACM Trans. Program. Lang. Syst. (TOPLAS) 18(3), 325\u2013353 (1996)","journal-title":"ACM Trans. Program. Lang. Syst. (TOPLAS)"},{"issue":"C","key":"1_CR63","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1016\/j.scico.2015.04.008","volume":"110","author":"D Murta","year":"2015","unstructured":"Murta, D., Oliveira, J.N.: A study of risk-aware program transformation. Sci. Comput. Program. 110(C), 51\u201377 (2015)","journal-title":"Sci. Comput. Program."},{"issue":"4","key":"1_CR64","doi-asserted-by":"crossref","first-page":"449","DOI":"10.1016\/j.jlamp.2015.11.007","volume":"85","author":"JN Oliveira","year":"2016","unstructured":"Oliveira, J.N., Miraldo, V.C.: \u201cKeep definition, change category\u201d \u2014 a practical approach to state-based system calculi. J. Logical Algebraic Methods Program. 85(4), 449\u2013474 (2016)","journal-title":"J. Logical Algebraic Methods Program."},{"key":"1_CR65","doi-asserted-by":"crossref","unstructured":"Pasareanu, C.S., Phan, Q., Malacaria, P.: Multi-run side-channel analysis using symbolic execution and Max-SMT. In: IEEE 29th Computer Security Foundations Symposium, CSF 2016, Lisbon, Portugal, 27 June\u20131 July 2016, pp. 387\u2013400 (2016)","DOI":"10.1109\/CSF.2016.34"},{"key":"1_CR66","doi-asserted-by":"crossref","unstructured":"P\u0103s\u0103reanu, C.S., Rungta, N.: Symbolic pathfinder: symbolic execution of Java bytecode. In: Proceedings of the IEEE\/ACM International Conference on Automated Software Engineering, pp. 179\u2013180. ACM (2010)","DOI":"10.1145\/1858996.1859035"},{"key":"1_CR67","doi-asserted-by":"crossref","DOI":"10.1515\/9783110809343","volume-title":"Mathematical Statistics: An Introduction","author":"WR Pestman","year":"1998","unstructured":"Pestman, W.R.: Mathematical Statistics: An Introduction, vol. 1. Walter de Gruyter, Berlin (1998)"},{"key":"1_CR68","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"527","DOI":"10.1007\/978-3-642-39799-8_35","volume-title":"Computer Aided Verification","author":"A Puggelli","year":"2013","unstructured":"Puggelli, A., Li, W., Sangiovanni-Vincentelli, A.L., Seshia, S.A.: Polynomial-time verification of PCTL properties of MDPs with convex uncertainties. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 527\u2013542. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-39799-8_35"},{"key":"1_CR69","doi-asserted-by":"crossref","DOI":"10.1002\/9780470316887","volume-title":"Markov Decision Processes: Discrete Stochastic Dynamic Programming","author":"ML Puterman","year":"1994","unstructured":"Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley, New York (1994)"},{"key":"1_CR70","doi-asserted-by":"crossref","unstructured":"Ramalingam, G.: Data flow frequency analysis. In: ACM SIGPLAN Notices, vol. 31, pp. 267\u2013277. ACM (1996)","DOI":"10.1145\/231379.231433"},{"key":"1_CR71","series-title":"Springer Texts in Statistics","volume-title":"The Bayesian Choice: From Decision-Theoretic Foundations to Computational Implementation","author":"C Robert","year":"2007","unstructured":"Robert, C.: The Bayesian Choice: From Decision-Theoretic Foundations to Computational Implementation. Springer Texts in Statistics. Springer, New York (2007)"},{"key":"1_CR72","volume-title":"Monte Carlo Statistical Methods","author":"C Robert","year":"2013","unstructured":"Robert, C., Casella, G.: Monte Carlo Statistical Methods. Springer, New York (2013)"},{"key":"1_CR73","volume-title":"Monte Carlo Statistical Methods","author":"CP Robert","year":"2005","unstructured":"Robert, C.P., Casella, G.: Monte Carlo Statistical Methods. Springer, New York (2005)"},{"key":"1_CR74","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"226","DOI":"10.1007\/11499107_17","volume-title":"Theory and Applications of Satisfiability Testing","author":"T Sang","year":"2005","unstructured":"Sang, T., Beame, P., Kautz, H.: Heuristics for fast exact model counting. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 226\u2013240. Springer, Heidelberg (2005). doi: 10.1007\/11499107_17"},{"key":"1_CR75","doi-asserted-by":"crossref","unstructured":"Schmidt, D.A.: Data flow analysis is model checking of abstract interpretations. In: Proceedings of the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 38\u201348. ACM (1998)","DOI":"10.1145\/268946.268950"},{"key":"1_CR76","doi-asserted-by":"crossref","unstructured":"Sen, K., Marinov, D., Agha, G.: CUTE: A concolic unit testing engine for C (2005)","DOI":"10.21236\/ADA482657"},{"issue":"3","key":"1_CR77","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1016\/j.entcs.2008.11.018","volume":"220","author":"MJ Smith","year":"2008","unstructured":"Smith, M.J.: Probabilistic abstract interpretation of imperative programs using truncated normal distributions. Electron. Notes Theor. Comput. Sci. 220(3), 43\u201359 (2008)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"1_CR78","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-89862-7_1","volume-title":"Information Systems Security","author":"D Song","year":"2008","unstructured":"Song, D., et al.: BitBlaze: a new approach to computer security via binary analysis. In: Sekar, R., Pujari, A.K. (eds.) ICISS 2008. LNCS, vol. 5352, pp. 1\u201325. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-89862-7_1"},{"key":"1_CR79","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/978-3-642-33125-1_10","volume-title":"Static Analysis","author":"A Thakur","year":"2012","unstructured":"Thakur, A., Elder, M., Reps, T.: Bilateral algorithms for symbolic abstraction. In: Min\u00e9, A., Schmidt, D. (eds.) SAS 2012. LNCS, vol. 7460, pp. 111\u2013128. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-33125-1_10"},{"key":"1_CR80","unstructured":"The Apache Software Foundation: Commons math. http:\/\/commons.apache.org\/proper\/commons-math\/ . Accessed 16 Dec 2014"},{"key":"1_CR81","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"424","DOI":"10.1007\/11814948_38","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2006","author":"M Thurley","year":"2006","unstructured":"Thurley, M.: sharpSAT \u2013 counting models with advanced component caching and implicit BCP. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 424\u2013429. Springer, Heidelberg (2006). doi: 10.1007\/11814948_38"},{"key":"1_CR82","first-page":"261","volume":"60","author":"LC Thurow","year":"1970","unstructured":"Thurow, L.C.: Analyzing the American income distribution. Am. Econ. Rev. 60, 261\u2013269 (1970)","journal-title":"Am. Econ. Rev."},{"key":"1_CR83","unstructured":"UC Davis, Mathematics: LattE. http:\/\/www.math.ucdavis.edu\/latte"},{"key":"1_CR84","unstructured":"Vall\u00e9e-Rai, R., Co, P., Gagnon, E., Hendren, L., Lam, P., Sundaresan, V.: Soot-a Java bytecode optimization framework. In: Proceedings of the 1999 Conference of the Centre for Advanced Studies on Collaborative Research, p. 13. IBM Press (1999)"},{"key":"1_CR85","unstructured":"Verdoolaege, S.: Software package barvinok (2004). http:\/\/freshmeat.net\/projects\/barvinok"},{"key":"1_CR86","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"362","DOI":"10.1007\/978-3-642-11319-2_26","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"B Wachter","year":"2010","unstructured":"Wachter, B., Zhang, L.: Best probabilistic transformers. In: Barthe, G., Hermenegildo, M. (eds.) VMCAI 2010. LNCS, vol. 5944, pp. 362\u2013379. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-11319-2_26"},{"key":"1_CR87","doi-asserted-by":"crossref","unstructured":"Zuliani, P., Platzer, A., Clarke, E.M.: Bayesian statistical model checking with application to simulink\/stateflow verification. In: Proceedings of the 13th ACM International Conference on Hybrid Systems: Computation and Control, pp. 243\u2013252. ACM (2010)","DOI":"10.1145\/1755952.1755987"}],"container-title":["Lecture Notes in Computer Science","Grand Timely Topics in Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-60074-1_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,30]],"date-time":"2022-07-30T03:22:49Z","timestamp":1659151369000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-60074-1_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319600734","9783319600741"],"references-count":87,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-60074-1_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}