{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:39:34Z","timestamp":1780994374854,"version":"3.54.1"},"publisher-location":"Cham","reference-count":46,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319415277","type":"print"},{"value":"9783319415284","type":"electronic"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"vor","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":[[2016]]},"DOI":"10.1007\/978-3-319-41528-4_4","type":"book-chapter","created":{"date-parts":[[2016,7,12]],"date-time":"2016-07-12T09:34:06Z","timestamp":1468316046000},"page":"62-83","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":108,"title":["PSI: Exact Symbolic Inference for Probabilistic Programs"],"prefix":"10.1007","author":[{"given":"Timon","family":"Gehr","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sasa","family":"Misailovic","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Martin","family":"Vechev","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2016,7,13]]},"reference":[{"key":"4_CR1","unstructured":"Maple (2015). www.maplesoft.com\/products\/maple\/"},{"key":"4_CR2","unstructured":"Maple Heaviside Function (2015). http:\/\/www.maplesoft.com\/support\/help\/Maple\/view.aspx?path=Heaviside"},{"key":"4_CR3","unstructured":"Mathematica (2015). https:\/\/www.wolfram.com\/mathematica\/"},{"issue":"8","key":"4_CR4","doi-asserted-by":"publisher","first-page":"568","DOI":"10.1016\/j.scico.2007.09.002","volume":"74","author":"P Audebaud","year":"2009","unstructured":"Audebaud, P., Paulin-Mohring, C.: Proofs of randomized algorithms in Coq. Sci. Comput. Program. 74(8), 568\u2013589 (2009)","journal-title":"Sci. Comput. Program."},{"key":"4_CR5","doi-asserted-by":"crossref","unstructured":"Barthe, G., K\u00f6pf, B., Olmedo, F., Zanella B\u00e9guelin, S.: Probabilistic relational reasoning for differential privacy. In: ACM POPL (2012)","DOI":"10.1145\/2103656.2103670"},{"key":"4_CR6","doi-asserted-by":"crossref","unstructured":"Bhat, S., Agarwal, A., Vuduc, R., Gray, A.: A type theory for probability density functions. In: ACM POPL (2012)","DOI":"10.1145\/2103656.2103721"},{"key":"4_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"508","DOI":"10.1007\/978-3-642-36742-7_35","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Bhat","year":"2013","unstructured":"Bhat, S., Borgstr\u00f6m, J., Gordon, A.D., Russo, C.: Deriving probability density functions from probabilistic functional programs. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol. 7795, pp. 508\u2013522. Springer, Heidelberg (2013)"},{"key":"4_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/978-3-642-19718-5_5","volume-title":"Programming Languages and Systems","author":"J Borgstr\u00f6m","year":"2011","unstructured":"Borgstr\u00f6m, J., Gordon, A.D., Greenberg, M., Margetson, J., Van Gael, J.: Measure transformer semantics for bayesian machine learning. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol. 6602, pp. 77\u201396. Springer, Heidelberg (2011)"},{"key":"4_CR9","doi-asserted-by":"crossref","unstructured":"Bornholt, J., Mytkowicz, T., McKinley, K.S.: Uncertain<T>: a first-order type for uncertain data. In: ASPLOS (2014)","DOI":"10.1145\/2541940.2541958"},{"key":"4_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-319-28228-2_9","volume-title":"Practical Aspects of Declarative Languages","author":"J Carette","year":"2016","unstructured":"Carette, J., Shan, C.-C.: Simplifying probabilistic programs using computer algebra. In: Gavanelli, M., et al. (eds.) PADL 2016. LNCS, vol. 9585, pp. 135\u2013152. Springer, Heidelberg (2016). doi: 10.1007\/978-3-319-28228-2_9"},{"issue":"6","key":"4_CR11","doi-asserted-by":"publisher","first-page":"910","DOI":"10.1109\/21.384253","volume":"25","author":"KC Chang","year":"1995","unstructured":"Chang, K.C., Fung, R.: Symbolic probabilistic inference with both discrete and continuous variables. IEEE Trans. Syst. Man Cybern. 25(6), 910\u2013916 (1995)","journal-title":"IEEE Trans. Syst. Man Cybern."},{"key":"4_CR12","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: ESEC\/FSE (2013)","DOI":"10.1145\/2491411.2491423"},{"issue":"2","key":"4_CR13","doi-asserted-by":"publisher","first-page":"393","DOI":"10.1016\/0004-3702(90)90060-D","volume":"42","author":"GF Cooper","year":"1990","unstructured":"Cooper, G.F.: The computational complexity of probabilistic inference using Bayesian belief networks. Artif. Intell. 42(2), 393\u2013405 (1990)","journal-title":"Artif. Intell."},{"key":"4_CR14","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.) Programming Languages and Systems. LNCS, vol. 7211, pp. 169\u2013193. Springer, Heidelberg (2012)"},{"issue":"1","key":"4_CR15","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1016\/0004-3702(93)90036-B","volume":"60","author":"P Dagum","year":"1993","unstructured":"Dagum, P., Luby, M.: Approximating probabilistic inference in Bayesian belief networks is NP-hard. Artif. Intell. 60(1), 141\u2013153 (1993)","journal-title":"Artif. Intell."},{"key":"4_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1007\/3-540-45605-8_15","volume-title":"Process Algebra and Probabilistic Methods. Performance Modeling and Verification","author":"A Di Pierro","year":"2002","unstructured":"Di Pierro, A., Wiklicky, H.: Probabilistic abstract interpretation and statistical testing (extended abstract). In: Hermanns, H., Segala, R. (eds.) PROBMIV 2002, PAPM-PROBMIV 2002 and PAPM 2002. LNCS, vol. 2399, p. 211. Springer, Heidelberg (2002)"},{"key":"4_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1007\/978-3-662-46669-8_4","volume-title":"Programming Languages and Systems","author":"M Eberl","year":"2015","unstructured":"Eberl, M., H\u00f6lzl, J., Nipkow, T.: A verified compiler for probability density functions. In: Vitek, J. (ed.) ESOP 2015. LNCS, vol. 9032, pp. 80\u2013104. Springer, Heidelberg (2015)"},{"key":"4_CR18","doi-asserted-by":"crossref","unstructured":"Filieri, A., P\u0103s\u0103reanu, C.S., Visser, W.: Reliability analysis in symbolic pathfinder. In: ICSE (2013)","DOI":"10.1109\/ICSE.2013.6606608"},{"key":"4_CR19","doi-asserted-by":"publisher","first-page":"530","DOI":"10.3102\/1076998615606113","volume":"40","author":"A Gelman","year":"2015","unstructured":"Gelman, A., Lee, D., Guo, J.: Stan a probabilistic programming language for Bayesian inference and optimization. J. Educ. Behav. Stat. 40, 530\u2013543 (2015)","journal-title":"J. Educ. Behav. Stat."},{"key":"4_CR20","doi-asserted-by":"publisher","first-page":"169","DOI":"10.2307\/2348941","volume":"43","author":"WR Gilks","year":"1994","unstructured":"Gilks, W.R., Thomas, A., Spiegelhalter, D.J.: A language and program for complex Bayesian modelling. Statistician 43, 169\u2013177 (1994)","journal-title":"Statistician"},{"key":"4_CR21","unstructured":"Goodman, N., Mansinghka, V., Roy, D., Bonawitz, K., Tenenbaum, J.: Church: a language for generative models. In: UAI (2008)"},{"key":"4_CR22","doi-asserted-by":"crossref","unstructured":"Gordon, A.D., Henzinger, T.A., Nori, A.V., Rajamani, S.K.: Probabilistic programming. In: Proceedings of Future of Software Engineering (2014)","DOI":"10.1145\/2593882.2593900"},{"key":"4_CR23","unstructured":"Gretz, F., Jansen, N., Kaminski, B.L., Katoen, J.P., McIver, A., Olmedo, F.: Conditioning in probabilistic programming. arXiv preprint (2015). arXiv:1504.00198"},{"key":"4_CR24","doi-asserted-by":"publisher","DOI":"10.4018\/978-1-4666-8315-0","volume-title":"Formalized Probability Theory and Applications Using Theorem Proving","author":"O Hasan","year":"2015","unstructured":"Hasan, O.: Formalized Probability Theory and Applications Using Theorem Proving. IGI Global, Hershey (2015)"},{"key":"4_CR25","unstructured":"Hershey, S., Bernstein, J., Bradley, B., Schweitzer, A., Stein, N., Weber, T., Vigoda, B.: Accelerating inference: towards a full language, compiler and hardware stack. arXiv preprint (2012). arXiv:1212.2991"},{"key":"4_CR26","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)"},{"key":"4_CR27","doi-asserted-by":"crossref","unstructured":"Hur, C.K., Nori, A.V., Rajamani, S.K., Samuel, S.: Slicing probabilistic programs. In: ACM PLDI (2014)","DOI":"10.1145\/2594291.2594303"},{"key":"4_CR28","unstructured":"Hurd, J.: Formal verification of probabilistic algorithms. Ph.D. thesis, University of Cambridge (2001)"},{"key":"4_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"390","DOI":"10.1007\/978-3-642-15769-1_24","volume-title":"Static Analysis","author":"J-P Katoen","year":"2010","unstructured":"Katoen, J.-P., McIver, A.K., Meinicke, L.A., Morgan, C.C.: Linear-invariant generation for probabilistic programs. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 390\u2013406. Springer, Heidelberg (2010)"},{"issue":"3","key":"4_CR30","doi-asserted-by":"publisher","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":"4_CR31","unstructured":"Kozlov, A.V., Koller, D.: Nonuniform dynamic discretization in hybrid networks. In: UAI (1997)"},{"key":"4_CR32","unstructured":"Mansinghka, V., Selsam, D., Perov, Y.: Venture: a higher-order probabilistic programming platform with programmable inference. arXiv preprint (2014). arXiv:1404.0099"},{"issue":"4","key":"4_CR33","doi-asserted-by":"publisher","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":"4_CR34","unstructured":"Minka, T., Winn, J., Guiver, J., Webster, S., Zaykov, Y., Yangel, B., Spengler, A., Bronskill, J.: Infer.NET 2.5 (2013). http:\/\/research.microsoft.com\/infernet"},{"key":"4_CR35","doi-asserted-by":"crossref","unstructured":"Monniaux, D.: Abstract interpretation of probabilistic semantics. In: SAS (2000)","DOI":"10.1007\/978-3-540-45099-3_17"},{"key":"4_CR36","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"156","DOI":"10.1007\/3-540-44652-4_15","volume-title":"Symbolic and Quantitative Approaches to Reasoning with Uncertainty","author":"S Moral","year":"2001","unstructured":"Moral, S., Rum\u00ed, R., Salmer\u00f3n, A.: Mixtures of truncated exponentials in hybrid Bayesian networks. In: Benferhat, S., Besnard, P. (eds.) ECSQARU 2001. LNCS (LNAI), vol. 2143, pp. 156\u2013167. Springer, Heidelberg (2001)"},{"issue":"3","key":"4_CR37","doi-asserted-by":"publisher","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)"},{"key":"4_CR38","unstructured":"Narayanan, P., Carette, J., Romano, W., Shan, C.C., Zinkov, R.: Probabilistic inference by program transformation in Hakaru (system description), http:\/\/homes.soic.indiana.edu\/ccshan\/rational\/system.pdf"},{"key":"4_CR39","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 (2014)","DOI":"10.1609\/aaai.v28i1.9060"},{"key":"4_CR40","unstructured":"Pfeffer, A.: IBAL: a probabilistic rational programming language. In: Proceedings of 17th International Joint Conference on Artificial Intelligence, vol. 1, pp. 733\u2013740. Morgan Kaufmann Publishers Inc. (2001)"},{"key":"4_CR41","doi-asserted-by":"crossref","unstructured":"Sampson, A., Panchekha, P., Mytkowicz, T., McKinley, K.S., Grossman, D., Ceze, L.: Expressing and verifying probabilistic assertions. In: ACM PLDI (2014)","DOI":"10.1145\/2594291.2594294"},{"key":"4_CR42","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: ACM PLDI (2013)","DOI":"10.1145\/2491956.2462179"},{"key":"4_CR43","unstructured":"Sanner, S., Abbasnejad, E.: Symbolic variable elimination for discrete and continuous graphical models. In: AAAI (2012)"},{"key":"4_CR44","unstructured":"Shachter, R.D., D\u2019Ambrosio, B., Del Favero, B.: Symbolic probabilistic inference in belief networks. In: AAAI (1990)"},{"issue":"5","key":"4_CR45","doi-asserted-by":"publisher","first-page":"641","DOI":"10.1016\/j.ijar.2010.09.003","volume":"52","author":"PP Shenoy","year":"2011","unstructured":"Shenoy, P.P., West, J.C.: Inference in hybrid Bayesian networks using mixtures of polynomials. Int. J. Approx. Reason. 52(5), 641\u2013657 (2011)","journal-title":"Int. J. Approx. Reason."},{"key":"4_CR46","unstructured":"Wood, F., van de Meent, J.W., Mansinghka, V.: A new approach to probabilistic programming inference. In: AISTATS (2014)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-41528-4_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,3]],"date-time":"2022-07-03T00:10:11Z","timestamp":1656807011000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-41528-4_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319415277","9783319415284"],"references-count":46,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-41528-4_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"13 July 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Toronto","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2016","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 July 2016","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23 July 2016","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2016","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}