{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:14:27Z","timestamp":1775873667966,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":82,"publisher":"ACM","license":[{"start":{"date-parts":[[2018,6,11]],"date-time":"2018-06-11T00:00:00Z","timestamp":1528675200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"a gift from Rajiv and Ritu Batra"},{"name":"AFRL under DARPA STAC award","award":["FA8750-15-C-0082"],"award-info":[{"award-number":["FA8750-15-C-0082"]}]},{"name":"AFRL under DARPA award","award":["FA8750-16-2-0274"],"award-info":[{"award-number":["FA8750-16-2-0274"]}]},{"name":"the Wisconsin Alumni Research Foundation"},{"name":"the UW-Madison Office of the Vice Chancellor for Research and Graduate Education"},{"name":"AFRL under DARPA MUSE award","award":["FA8750-14-2-0270"],"award-info":[{"award-number":["FA8750-14-2-0270"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2018,6,11]]},"DOI":"10.1145\/3192366.3192408","type":"proceedings-article","created":{"date-parts":[[2018,6,12]],"date-time":"2018-06-12T08:16:01Z","timestamp":1528791361000},"page":"513-528","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":18,"title":["PMAF: an algebraic framework for static analysis of probabilistic programs"],"prefix":"10.1145","author":[{"given":"Di","family":"Wang","sequence":"first","affiliation":[{"name":"Carnegie Mellon University, USA"}]},{"given":"Jan","family":"Hoffmann","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, USA"}]},{"given":"Thomas","family":"Reps","sequence":"additional","affiliation":[{"name":"University of Wisconsin, USA \/ GrammaTech, USA"}]}],"member":"320","published-online":{"date-parts":[[2018,6,11]]},"reference":[{"key":"e_1_3_2_2_1_1","doi-asserted-by":"crossref","unstructured":"S. Abramsky and A. Jung. 1994. Domain Theory. In Handbook of Logic in Computer Science. Oxford University Press Oxford UK. S. Abramsky and A. Jung. 1994. Domain Theory. In Handbook of Logic in Computer Science . Oxford University Press Oxford UK.","DOI":"10.1093\/oso\/9780198537625.003.0001"},{"key":"e_1_3_2_2_2_1","doi-asserted-by":"crossref","unstructured":"R. I. Bahar E. A. Frohm C. M. Gaona G. D. Hachtel E. Macii A. Pardo and F. Somenzi. 1997. Algebraic Decision Diagrams and their Applications. Formal Methods in System Design 10 (April 1997). Issue 2. R. I. Bahar E. A. Frohm C. M. Gaona G. D. Hachtel E. Macii A. Pardo and F. Somenzi. 1997. Algebraic Decision Diagrams and their Applications. Formal Methods in System Design 10 (April 1997). Issue 2.","DOI":"10.1023\/A:1008699807402"},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"crossref","unstructured":"T. Ball A. Podelski and S. K. Rajamani. 2001. Boolean and Cartesian Abstraction for Model Checking C Programs. In Tools and Algs. for the Construct. and Anal. of Syst. (TACAS'01). T. Ball A. Podelski and S. K. Rajamani. 2001. Boolean and Cartesian Abstraction for Model Checking C Programs. In Tools and Algs. for the Construct. and Anal. of Syst. (TACAS'01) .","DOI":"10.1007\/3-540-45319-9_19"},{"key":"e_1_3_2_2_4_1","volume":"201","author":"Barthe G.","unstructured":"G. Barthe , T. Espitau , L. M. Ferrer Fioriti , and J. Hsu. 201 6. Synthesizing Probabilistic Invariants via Doob's Decomposition. In Computer Aided Verif. (CAV'16). G. Barthe, T. Espitau, L. M. Ferrer Fioriti, and J. Hsu. 2016. Synthesizing Probabilistic Invariants via Doob's Decomposition. In Computer Aided Verif. (CAV'16).","journal-title":"J. Hsu."},{"key":"e_1_3_2_2_5_1","unstructured":"G. Barthe T. Espitau M. Gaboardi B. Gregoire J. Hsu and P.-Y. Strub. 2016. A Program Logic for Probabilistic Programs. Available at justinh.su\/files\/papers\/ellora.pdf. G. Barthe T. Espitau M. Gaboardi B. Gregoire J. Hsu and P.-Y. Strub. 2016. A Program Logic for Probabilistic Programs. Available at justinh.su\/files\/papers\/ellora.pdf."},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"crossref","unstructured":"G. Barthe B. Gregoire and S. Zanella Beguelin. 2009. Formal Certification of Code-based Cryptographic Proofs. In Princ. of Prog. Lang. (POPL'09). G. Barthe B. Gregoire and S. Zanella Beguelin. 2009. Formal Certification of Code-based Cryptographic Proofs. In Princ. of Prog. Lang. (POPL'09) .","DOI":"10.1145\/1480881.1480894"},{"key":"e_1_3_2_2_7_1","volume-title":"Probability and Measure","author":"Billingsley P.","unstructured":"P. Billingsley . 2012. Probability and Measure . John Wiley & Sons, Inc. P. Billingsley. 2012. Probability and Measure. John Wiley & Sons, Inc."},{"key":"e_1_3_2_2_8_1","volume-title":"Int. Conf. on Functional Programming (ICFP'16)","author":"Borgstrom J.","unstructured":"J. Borgstrom , U. D. Lago , A. D. Gordon , and M. Szymczak . 2016. A Lambda-Calculus Foundation for Universal Probabilistic Programming . In Int. Conf. on Functional Programming (ICFP'16) . J. Borgstrom, U. D. Lago, A. D. Gordon, and M. Szymczak. 2016. A Lambda-Calculus Foundation for Universal Probabilistic Programming. In Int. Conf. on Functional Programming (ICFP'16)."},{"key":"e_1_3_2_2_9_1","unstructured":"F. Bourdoncle. 1993. Efficient Chaotic Iteration Strategies With Widenings. In Formal Methods in Prog. and Their Applications. F. Bourdoncle. 1993. Efficient Chaotic Iteration Strategies With Widenings. In Formal Methods in Prog. and Their Applications ."},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"crossref","unstructured":"T. Brazdil S. Kiefer and A. Kucera. 2014. Efficient Analysis of Probabilistic Programs with an Unbounded Counter. J. ACM 61 (November 2014). Issue 6. T. Brazdil S. Kiefer and A. Kucera. 2014. Efficient Analysis of Probabilistic Programs with an Unbounded Counter. J. ACM 61 (November 2014). Issue 6.","DOI":"10.1145\/2629599"},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"crossref","unstructured":"T. Brazdil S. Kiefer A. Kucera and I. H. Varekova. 2015. Runtime Analysis of Probabilistic Programs with Unbounded Recursion. J. Comput. Syst. Sci. 81 (February 2015). Issue 1. T. Brazdil S. Kiefer A. Kucera and I. H. Varekova. 2015. Runtime Analysis of Probabilistic Programs with Unbounded Recursion. J. Comput. Syst. Sci. 81 (February 2015). Issue 1.","DOI":"10.1016\/j.jcss.2014.06.005"},{"key":"e_1_3_2_2_12_1","volume-title":"Stan: A Probabilistic Programming Language. J. Statistical Softw. 76","author":"Carpenter B.","year":"2017","unstructured":"B. Carpenter , A. Gelman , M. D. Hoffman , D. Lee , B. Goodrich , M. Betancourt , M. Brubaker , J. Guo , P. Li , and A. Riddell . 2017 . Stan: A Probabilistic Programming Language. J. Statistical Softw. 76 (2017). Issue 1. B. Carpenter, A. Gelman, M. D. Hoffman, D. Lee, B. Goodrich, M. Betancourt, M. Brubaker, J. Guo, P. Li, and A. Riddell. 2017. Stan: A Probabilistic Programming Language. J. Statistical Softw. 76 (2017). Issue 1."},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"crossref","unstructured":"A. Chakarov and S. Sankaranarayanan. 2013. Probabilistic Program Analysis with Martingales. In Computer Aided Verif. (CAV'13). A. Chakarov and S. Sankaranarayanan. 2013. Probabilistic Program Analysis with Martingales. In Computer Aided Verif. (CAV'13) .","DOI":"10.1007\/978-3-642-39799-8_34"},{"key":"e_1_3_2_2_14_1","volume-title":"Static Analysis Symp. (SAS'14)","author":"Chakarov A.","unstructured":"A. Chakarov and S. Sankaranarayanan . 2014. Expectation Invariants for Probabilistic Program Loops as Fixed Points . In Static Analysis Symp. (SAS'14) . A. Chakarov and S. Sankaranarayanan. 2014. Expectation Invariants for Probabilistic Program Loops as Fixed Points. In Static Analysis Symp. (SAS'14)."},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"crossref","unstructured":"K. Chatterjee H. Fu and A. K. Goharshady. 2016. Termination Analysis of Probabilistic Programs Through Positivstellensatz's. In Computer Aided Verif. (CAV'16). K. Chatterjee H. Fu and A. K. Goharshady. 2016. Termination Analysis of Probabilistic Programs Through Positivstellensatz's. In Computer Aided Verif. (CAV'16) .","DOI":"10.1007\/978-3-319-41528-4_1"},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"crossref","unstructured":"K. Chatterjee H. Fu P. Novotny and R. Hasheminezhad. 2016. Algorithmic Analysis of Qualitative and Quantitative Termination Problems for Affine Probabilistic Programs. In Princ. of Prog. Lang. (POPL'16). K. Chatterjee H. Fu P. Novotny and R. Hasheminezhad. 2016. Algorithmic Analysis of Qualitative and Quantitative Termination Problems for Affine Probabilistic Programs. In Princ. of Prog. Lang. (POPL'16) .","DOI":"10.1145\/2837614.2837639"},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"crossref","unstructured":"K. Chatterjee P. Novotny and D. ?ikelic. 2017. Stochastic Invariants for Probabilistic Termination. In Princ. of Prog. Lang. (POPL'17). K. Chatterjee P. Novotny and D. ?ikelic. 2017. Stochastic Invariants for Probabilistic Termination. In Princ. of Prog. Lang. (POPL'17) .","DOI":"10.1145\/3009837.3009873"},{"key":"e_1_3_2_2_18_1","volume":"201","author":"Claret G.","unstructured":"G. Claret , S. K. Rajamani , A. V. Nori , A. D. Gordon , and J. Borgstrom. 201 3. Bayesian Inference using Data Flow Analysis. In Found. of Softw. Eng. (FSE'13). G. Claret, S. K. Rajamani, A. V. Nori, A. D. Gordon, and J. Borgstrom. 2013. Bayesian Inference using Data Flow Analysis. In Found. of Softw. Eng. (FSE'13).","journal-title":"J. Borgstrom."},{"key":"e_1_3_2_2_19_1","volume":"200","author":"Conchon S.","unstructured":"S. Conchon , J.-C. Filliatre , and J. Signoles. 200 7. Designing a Generic Graph Library Using ML Functors. In Trends in Functional Programming. S. Conchon, J.-C. Filliatre, and J. Signoles. 2007. Designing a Generic Graph Library Using ML Functors. In Trends in Functional Programming.","journal-title":"J. Signoles."},{"key":"e_1_3_2_2_20_1","volume-title":"Program Flow Analysis: Theory and Applications","author":"Cousot P.","unstructured":"P. Cousot . 1981. Semantic Foundations of Program Analysis . In Program Flow Analysis: Theory and Applications . Prentice-Hall . P. Cousot. 1981. Semantic Foundations of Program Analysis. In Program Flow Analysis: Theory and Applications. Prentice-Hall."},{"key":"e_1_3_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_3_2_2_22_1","volume-title":"St","author":"Cousot P.","year":"1977","unstructured":"P. Cousot and R. Cousot . 1978. Static Determination of Dynamic Properties of Recursive Procedures. In Formal Descriptions of Programming Concepts, (IFIP WG 2.2 , St . Andrews, Canada , August 1977 ). North-Holland. P. Cousot and R. Cousot. 1978. Static Determination of Dynamic Properties of Recursive Procedures. In Formal Descriptions of Programming Concepts, (IFIP WG 2.2, St. Andrews, Canada, August 1977). North-Holland."},{"key":"e_1_3_2_2_23_1","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. 1979. Systematic Design of Program Analysis Frameworks. In Princ. of Prog. Lang. (POPL'79). P. Cousot and R. Cousot. 1979. Systematic Design of Program Analysis Frameworks. In Princ. of Prog. Lang. (POPL'79) .","DOI":"10.1145\/567752.567778"},{"key":"e_1_3_2_2_24_1","doi-asserted-by":"crossref","unstructured":"P. Cousot and N. Halbwachs. 1978. Automatic Discovery of Linear Constraints Among Variables of a Program. In Princ. of Prog. Lang. (POPL'78). P. Cousot and N. Halbwachs. 1978. Automatic Discovery of Linear Constraints Among Variables of a Program. In Princ. of Prog. Lang. (POPL'78) .","DOI":"10.1145\/512760.512770"},{"key":"e_1_3_2_2_25_1","volume-title":"Probabilistic Abstract Interpretation. In European Symp. on Programming (ESOP'12)","author":"Cousot P.","unstructured":"P. Cousot and M. Monerau . 2012 . Probabilistic Abstract Interpretation. In European Symp. on Programming (ESOP'12) . P. Cousot and M. Monerau. 2012. Probabilistic Abstract Interpretation. In European Symp. on Programming (ESOP'12)."},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"crossref","unstructured":"E. Darulova and V. Kuncak. 2014. Sound Compilation of Reals. In Princ. of Prog. Lang. (POPL'14). E. Darulova and V. Kuncak. 2014. Sound Compilation of Reals. In Princ. of Prog. Lang. (POPL'14) .","DOI":"10.1145\/2535838.2535874"},{"key":"e_1_3_2_2_27_1","volume-title":"Mixing Up Nondeterminism and Probability: a preliminary report. Electr. Notes Theor. Comp. Sci. 22","author":"den Hartog J. I.","year":"1999","unstructured":"J. I. den Hartog and E. P. de Vink . 1999. Mixing Up Nondeterminism and Probability: a preliminary report. Electr. Notes Theor. Comp. Sci. 22 ( 1999 ). J. I. den Hartog and E. P. de Vink. 1999. Mixing Up Nondeterminism and Probability: a preliminary report. Electr. Notes Theor. Comp. Sci. 22 (1999)."},{"key":"e_1_3_2_2_28_1","volume-title":"A Discipline of Programming","author":"Dijkstra E. W.","unstructured":"E. W. Dijkstra . 1997. A Discipline of Programming . Prentice Hall PTR Upper Saddle River . E. W. Dijkstra. 1997. A Discipline of Programming. Prentice Hall PTR Upper Saddle River."},{"key":"e_1_3_2_2_29_1","volume-title":"Recursive Stochastic Games with Positive Rewards. In Int. Colloq. on Automata, Langs., and Programming (ICALP'08)","author":"Etessami K.","unstructured":"K. Etessami , D. Wojtczak , and M. Yannakakis . 2008 . Recursive Stochastic Games with Positive Rewards. In Int. Colloq. on Automata, Langs., and Programming (ICALP'08) . K. Etessami, D.Wojtczak, and M. Yannakakis. 2008. Recursive Stochastic Games with Positive Rewards. In Int. Colloq. on Automata, Langs., and Programming (ICALP'08)."},{"key":"e_1_3_2_2_30_1","volume-title":"Symp. on Theor. Aspects of Comp. Sci. (STACS'05)","author":"Etessami K.","unstructured":"K. Etessami and M. Yannakakis . 2005. Recursive Markov Chains, Stochastic Grammars, and Monotone Systems of Nonlinear Equations . In Symp. on Theor. Aspects of Comp. Sci. (STACS'05) . K. Etessami and M. Yannakakis. 2005. Recursive Markov Chains, Stochastic Grammars, and Monotone Systems of Nonlinear Equations. In Symp. on Theor. Aspects of Comp. Sci. (STACS'05)."},{"key":"e_1_3_2_2_31_1","doi-asserted-by":"crossref","unstructured":"K. Etessami and M. Yannakakis. 2015. Recursive Markov Decision Processes and Recursive Stochastic Games. J. ACM 62 (May 2015). Issue 2. K. Etessami and M. Yannakakis. 2015. Recursive Markov Decision Processes and Recursive Stochastic Games. J. ACM 62 (May 2015). Issue 2.","DOI":"10.1145\/2699431"},{"key":"e_1_3_2_2_32_1","doi-asserted-by":"crossref","unstructured":"A. Farzan and Z. Kincaid. 2015. Compositional Recurrence Analysis. In Formal Methods in Compiter-Aided Design (FMCAD'15). A. Farzan and Z. Kincaid. 2015. Compositional Recurrence Analysis. In Formal Methods in Compiter-Aided Design (FMCAD'15) .","DOI":"10.1109\/FMCAD.2015.7542253"},{"key":"e_1_3_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677001"},{"key":"e_1_3_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"e_1_3_2_2_35_1","doi-asserted-by":"crossref","unstructured":"G. Gallo G. Longo S. Pallottino and S. Nguyen. 1993. Directed Hypergraphs and Applications. Disc. Appl. Math. 42 (April 1993). Issue 2. G. Gallo G. Longo S. Pallottino and S. Nguyen. 1993. Directed Hypergraphs and Applications. Disc. Appl. Math. 42 (April 1993). Issue 2.","DOI":"10.1016\/0166-218X(93)90045-P"},{"key":"e_1_3_2_2_36_1","volume-title":"PSI: Exact Symbolic Inference for Probabilistic Programs. In Computer Aided Verif. (CAV'16).","author":"Gehr T.","year":"2016","unstructured":"T. Gehr , S. Misailovic , and M. Vechev . 2016 . PSI: Exact Symbolic Inference for Probabilistic Programs. In Computer Aided Verif. (CAV'16). T. Gehr, S. Misailovic, and M. Vechev. 2016. PSI: Exact Symbolic Inference for Probabilistic Programs. In Computer Aided Verif. (CAV'16)."},{"key":"e_1_3_2_2_37_1","volume-title":"Probabilistic machine learning and artificial intelligence. Nature","author":"Ghahramani Z.","year":"2015","unstructured":"Z. Ghahramani . 2015. Probabilistic machine learning and artificial intelligence. Nature ( 2015 ). Z. Ghahramani. 2015. Probabilistic machine learning and artificial intelligence. Nature (2015)."},{"key":"e_1_3_2_2_38_1","unstructured":"N. D. Goodman V. K. Mansinghka D. M. Roy and J. B. Tenenbaum. 2008. Church: a language for generative models. In Uncertainty in Artif. Intelligence. N. D. Goodman V. K. Mansinghka D. M. Roy and J. B. Tenenbaum. 2008. Church: a language for generative models. In Uncertainty in Artif. Intelligence ."},{"key":"e_1_3_2_2_39_1","doi-asserted-by":"crossref","unstructured":"A. D. Gordon T. A. Henzinger A. V. Nori and S. K. Rajamani. 2014. Probabilistic Programming. In Future of Softw. Eng. (FOSE'14). A. D. Gordon T. A. Henzinger A. V. Nori and S. K. Rajamani. 2014. Probabilistic Programming. In Future of Softw. Eng. (FOSE'14) .","DOI":"10.1145\/2593882.2593900"},{"key":"e_1_3_2_2_40_1","doi-asserted-by":"crossref","unstructured":"S. Graf and H. Saidi. 1997. Construction of Abstract State Graphs with PVS. In Computer Aided Verif. (CAV'97). S. Graf and H. Saidi. 1997. Construction of Abstract State Graphs with PVS. In Computer Aided Verif. (CAV'97) .","DOI":"10.1007\/3-540-63166-6_10"},{"key":"e_1_3_2_2_41_1","doi-asserted-by":"crossref","unstructured":"C. A. Gunter P. D. Mosses and D. S. Scott. 1989. Semantic Domains and Denotational Semantics. Technical Report. University of Pennsylvania Department of Computer and Information Science. C. A. Gunter P. D. Mosses and D. S. Scott. 1989. Semantic Domains and Denotational Semantics . Technical Report. University of Pennsylvania Department of Computer and Information Science.","DOI":"10.21236\/ADA220285"},{"key":"e_1_3_2_2_43_1","volume-title":"An Axiomatic Basis for Computer Programming. Commun. ACM 12 (October","author":"Hoare C. A. R.","year":"1969","unstructured":"C. A. R. Hoare . 1969. An Axiomatic Basis for Computer Programming. Commun. ACM 12 (October 1969 ). Issue 10. C. A. R. Hoare. 1969. An Axiomatic Basis for Computer Programming. Commun. ACM 12 (October 1969). Issue 10."},{"key":"e_1_3_2_2_44_1","doi-asserted-by":"crossref","unstructured":"S. Horwitz T. Reps and M. Sagiv. 1995. Demand Interprocedural Dataflow Analysis. In Found. of Softw. Eng. (FSE'95). S. Horwitz T. Reps and M. Sagiv. 1995. Demand Interprocedural Dataflow Analysis. In Found. of Softw. Eng. (FSE'95) .","DOI":"10.1145\/222124.222146"},{"key":"e_1_3_2_2_45_1","volume-title":"Apron: A Library of Numerical Abstract Domains for Static Analysis. In Computer Aided Verif. (CAV'09).","author":"Jeannet B.","year":"2009","unstructured":"B. Jeannet and A. Mine . 2009 . Apron: A Library of Numerical Abstract Domains for Static Analysis. In Computer Aided Verif. (CAV'09). B. Jeannet and A. Mine. 2009. Apron: A Library of Numerical Abstract Domains for Static Analysis. In Computer Aided Verif. (CAV'09)."},{"key":"e_1_3_2_2_46_1","unstructured":"C. Jones. 1989. Probabilistic Non-determinism. Ph.D. Dissertation. University of Edinburgh Edinburgh. C. Jones. 1989. Probabilistic Non-determinism . Ph.D. Dissertation. University of Edinburgh Edinburgh."},{"key":"e_1_3_2_2_47_1","unstructured":"C. Jones and G. Plotkin. 1989. A Probabilistic Powerdomain of Evaluations. In Logic in Computer Science (LICS'89). C. Jones and G. Plotkin. 1989. A Probabilistic Powerdomain of Evaluations. In Logic in Computer Science (LICS'89) ."},{"key":"e_1_3_2_2_48_1","volume-title":"Weakest Precondition Reasoning for Expected Run--Times of Probabilistic Programs. In European Symp. on Programming (ESOP'16)","author":"Kaminski B. L.","unstructured":"B. L. Kaminski , J.-P. Katoen , C. Matheja , and F. Olmedo . 2016 . Weakest Precondition Reasoning for Expected Run--Times of Probabilistic Programs. In European Symp. on Programming (ESOP'16) . B. L. Kaminski, J.-P. Katoen, C. Matheja, and F. Olmedo. 2016. Weakest Precondition Reasoning for Expected Run--Times of Probabilistic Programs. In European Symp. on Programming (ESOP'16)."},{"key":"e_1_3_2_2_49_1","volume-title":"Linear-Invariant Generation for Probabilistic Programs: Automated Support for Proof-Based Methods. In Static Analysis Symp. (SAS'10)","author":"Katoen J.-P.","unstructured":"J.-P. Katoen , A. K. McIver , L. A. Meinicke , and C. C. Morgan . 2010 . Linear-Invariant Generation for Probabilistic Programs: Automated Support for Proof-Based Methods. In Static Analysis Symp. (SAS'10) . J.-P. Katoen, A. K. McIver, L. A. Meinicke, and C. C. Morgan. 2010. Linear-Invariant Generation for Probabilistic Programs: Automated Support for Proof-Based Methods. In Static Analysis Symp. (SAS'10)."},{"key":"e_1_3_2_2_50_1","doi-asserted-by":"crossref","unstructured":"M. Kattenbelt M. Kwiatkowska G. Norman and D. Parker. 2009. Abstraction Refinement for Probabilistic Software. In Verif. Model Checking and Abs. Interp. (VMCAI'09). M. Kattenbelt M. Kwiatkowska G. Norman and D. Parker. 2009. Abstraction Refinement for Probabilistic Software. In Verif. Model Checking and Abs. Interp. (VMCAI'09) .","DOI":"10.1007\/978-3-540-93900-9_17"},{"key":"e_1_3_2_2_51_1","doi-asserted-by":"crossref","unstructured":"G. A. Kildall. 1973. A Unified Approach to Global Program Optimization. In Princ. of Prog. Lang. (POPL'73). G. A. Kildall. 1973. A Unified Approach to Global Program Optimization. In Princ. of Prog. Lang. (POPL'73) .","DOI":"10.1145\/512927.512945"},{"key":"e_1_3_2_2_52_1","doi-asserted-by":"crossref","unstructured":"J. Knoop and B. Steffen. 1992. The Interprocedural Coincidence Theorem. In Comp. Construct. (CC'92). J. Knoop and B. Steffen. 1992. The Interprocedural Coincidence Theorem. In Comp. Construct. (CC'92) .","DOI":"10.1007\/3-540-55984-1_13"},{"key":"e_1_3_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(77)90002-3"},{"key":"e_1_3_2_2_54_1","unstructured":"S. Kok M. Sumner M. Richardson P. Singla H. Poon D. Lowd J. Wang and P. Domingos. 2007. The Alchemy System for Statistical Relational AI. Technical Report. University of Washington. S. Kok M. Sumner M. Richardson P. Singla H. Poon D. Lowd J. Wang and P. Domingos. 2007. The Alchemy System for Statistical Relational AI . Technical Report. University of Washington."},{"key":"e_1_3_2_2_55_1","volume-title":"Semantics of Probabilistic Programs. J. Comput. Syst. Sci. 22 (June","author":"Kozen D.","year":"1981","unstructured":"D. Kozen . 1981. Semantics of Probabilistic Programs. J. Comput. Syst. Sci. 22 (June 1981 ). Issue 3. D. Kozen. 1981. Semantics of Probabilistic Programs. J. Comput. Syst. Sci. 22 (June 1981). Issue 3."},{"key":"e_1_3_2_2_56_1","doi-asserted-by":"crossref","unstructured":"D. Kozen. 1985. A Probabilistic PDL. J. Comput. Syst. Sci. 30 (April 1985). Issue 2. D. Kozen. 1985. A Probabilistic PDL. J. Comput. Syst. Sci. 30 (April 1985). Issue 2.","DOI":"10.1016\/0022-0000(85)90012-1"},{"key":"e_1_3_2_2_57_1","doi-asserted-by":"crossref","unstructured":"A. Lal T. Reps and G. Balakrishnan. 2005. Extended Weighted Pushdown Systems. In Computer Aided Verif. (CAV'05). A. Lal T. Reps and G. Balakrishnan. 2005. Extended Weighted Pushdown Systems. In Computer Aided Verif. (CAV'05) .","DOI":"10.1007\/11513988_44"},{"key":"e_1_3_2_2_58_1","volume":"200","author":"Li Z.","unstructured":"Z. Li and J. Eisner. 200 9. First- and Second-Order Expectation Semirings with Applications to Minimum-Risk Training on Translation Forests. In Conference on Empirical Methods in Natural Language Processing (EMNLP'09). Z. Li and J. Eisner. 2009. First- and Second-Order Expectation Semirings with Applications to Minimum-Risk Training on Translation Forests. In Conference on Empirical Methods in Natural Language Processing (EMNLP'09).","journal-title":"J. Eisner."},{"key":"e_1_3_2_2_59_1","doi-asserted-by":"crossref","unstructured":"A. K. McIver and C. C. Morgan. 2001. Partial correctness for probabilistic demonic programs. Theor. Comp. Sci. 266 (September 2001). Issue 1. A. K. McIver and C. C. Morgan. 2001. Partial correctness for probabilistic demonic programs. Theor. Comp. Sci. 266 (September 2001). Issue 1.","DOI":"10.1016\/S0304-3975(00)00208-5"},{"key":"e_1_3_2_2_60_1","doi-asserted-by":"crossref","unstructured":"A. K. McIver and C. C. Morgan. 2005. Abstraction Refinement and Proof for Probabilistic Systems. Springer Science+Business Media Inc. A. K. McIver and C. C. Morgan. 2005. Abstraction Refinement and Proof for Probabilistic Systems . Springer Science+Business Media Inc.","DOI":"10.1145\/1059816.1059824"},{"key":"e_1_3_2_2_61_1","volume-title":"BLOG: Probabilistic Models with Unknown Objects. In Int. Joint Conf. on Artif. Intelligence (IJCAI'05)","author":"Milch B.","unstructured":"B. Milch , B. Marthi , S. Russell , D. Sontag , D. L. Ong , and A. Kolobov . 2005 . BLOG: Probabilistic Models with Unknown Objects. In Int. Joint Conf. on Artif. Intelligence (IJCAI'05) . B. Milch, B. Marthi, S. Russell, D. Sontag, D. L. Ong, and A. Kolobov. 2005. BLOG: Probabilistic Models with Unknown Objects. In Int. Joint Conf. on Artif. Intelligence (IJCAI'05)."},{"key":"e_1_3_2_2_62_1","unstructured":"A. Mine. 2006. Symbolic Methods to Enhance the Precision of Numerical Abstract Domains. In Verif. Model Checking and Abs. Interp. (VMCAI'06). A. Mine. 2006. Symbolic Methods to Enhance the Precision of Numerical Abstract Domains. In Verif. Model Checking and Abs. Interp. (VMCAI'06) ."},{"key":"e_1_3_2_2_63_1","volume":"201","author":"Minka T.","unstructured":"T. Minka , J. M. Winn , J. P. Guiver , S. Webster , Y. Zaykov , B. Yangel , A. Spengler , and J. Bronskill. 201 4. Infer.NET 2.6. Microsoft Research Cambridge. research.microsoft.com\/infernet. T. Minka, J. M. Winn, J. P. Guiver, S. Webster, Y. Zaykov, B. Yangel, A. Spengler, and J. Bronskill. 2014. Infer.NET 2.6. Microsoft Research Cambridge. research.microsoft.com\/infernet.","journal-title":"J. Bronskill."},{"key":"e_1_3_2_2_64_1","doi-asserted-by":"crossref","unstructured":"M. Mislove. 2000. Nondeterminism and Probabilistic Choice: Obeying the Laws. In Concurrency Theory. M. Mislove. 2000. Nondeterminism and Probabilistic Choice: Obeying the Laws. In Concurrency Theory .","DOI":"10.1007\/3-540-44618-4_26"},{"key":"e_1_3_2_2_65_1","volume":"200","author":"Mislove M.","unstructured":"M. Mislove , J. Ouaknine , and J. Worrell. 200 4. Axioms for Probability and Nondeterminism. Electr. Notes Theor. Comp. Sci. 96 (June 2004). M. Mislove, J. Ouaknine, and J. Worrell. 2004. Axioms for Probability and Nondeterminism. Electr. Notes Theor. Comp. Sci. 96 (June 2004).","journal-title":"J. Worrell."},{"key":"e_1_3_2_2_66_1","doi-asserted-by":"crossref","unstructured":"U. Moncke and R. Wilhelm. 1991. Grammar Flow Analysis. In Attribute Grammars Applications and Systems (Int. Summer School SAGA). U. Moncke and R. Wilhelm. 1991. Grammar Flow Analysis. In Attribute Grammars Applications and Systems (Int. Summer School SAGA) .","DOI":"10.1007\/3-540-54572-7_6"},{"key":"e_1_3_2_2_67_1","volume-title":"Abstract Interpretation of Probabilistic Semantics. In Static Analysis Symp. (SAS'00)","author":"Monniaux D.","year":"2000","unstructured":"D. Monniaux . 2000 . Abstract Interpretation of Probabilistic Semantics. In Static Analysis Symp. (SAS'00) . D. Monniaux. 2000. Abstract Interpretation of Probabilistic Semantics. In Static Analysis Symp. (SAS'00)."},{"key":"e_1_3_2_2_68_1","volume-title":"Backwards Abstract Interpretation of Probabilistic Programs. In European Symp. on Programming (ESOP'01)","author":"Monniaux D.","year":"2001","unstructured":"D. Monniaux . 2001 . Backwards Abstract Interpretation of Probabilistic Programs. In European Symp. on Programming (ESOP'01) . D. Monniaux. 2001. Backwards Abstract Interpretation of Probabilistic Programs. In European Symp. on Programming (ESOP'01)."},{"key":"e_1_3_2_2_69_1","doi-asserted-by":"publisher","DOI":"10.5555\/1760267.1760285"},{"key":"e_1_3_2_2_70_1","unstructured":"M. Mottl. 2017. Lacaml - Linear Algebra for OCaml. Available at github.com\/mmottl\/lacaml. M. Mottl. 2017. Lacaml - Linear Algebra for OCaml. Available at github.com\/mmottl\/lacaml."},{"key":"e_1_3_2_2_71_1","doi-asserted-by":"crossref","unstructured":"M. Muller-Olm and H. Seidl. 2004. Precise Interprocedural Analysis through Linear Algebra. In Princ. of Prog. Lang. (POPL'04). M. Muller-Olm and H. Seidl. 2004. Precise Interprocedural Analysis through Linear Algebra. In Princ. of Prog. Lang. (POPL'04) .","DOI":"10.1145\/964001.964029"},{"key":"e_1_3_2_2_72_1","doi-asserted-by":"crossref","unstructured":"F. Olmedo B. L. Kaminski J.-P. Katoen and C. Matheja. 2016. Reasoning about Recursive Probabilistic Programs. In Logic in Computer Science (LICS'16). F. Olmedo B. L. Kaminski J.-P. Katoen and C. Matheja. 2016. Reasoning about Recursive Probabilistic Programs. In Logic in Computer Science (LICS'16) .","DOI":"10.1145\/2933575.2935317"},{"key":"e_1_3_2_2_73_1","volume-title":"The Category of Markov Kernels. Electr. Notes Theor. Comp. Sci. 22","author":"Panangaden P.","year":"1999","unstructured":"P. Panangaden . 1999. The Category of Markov Kernels. Electr. Notes Theor. Comp. Sci. 22 ( 1999 ). P. Panangaden. 1999. The Category of Markov Kernels. Electr. Notes Theor. Comp. Sci. 22 (1999)."},{"key":"e_1_3_2_2_75_1","volume-title":"Markov Decision Processes: Discrete Stochastic Dynamic Programming","author":"Puterman M. L.","unstructured":"M. L. Puterman . 1994. Markov Decision Processes: Discrete Stochastic Dynamic Programming . John Wiley & Sons, Inc. M. L. Puterman. 1994. Markov Decision Processes: Discrete Stochastic Dynamic Programming. John Wiley & Sons, Inc."},{"key":"e_1_3_2_2_76_1","volume-title":"Bounded Incremental Computation","author":"Ramalingam G.","unstructured":"G. Ramalingam . 1996. Bounded Incremental Computation . Springer-Verlag . G. Ramalingam. 1996. Bounded Incremental Computation. Springer-Verlag."},{"key":"e_1_3_2_2_77_1","doi-asserted-by":"crossref","unstructured":"T. Reps S. Horwitz and M. Sagiv. 1995. Precise Interprocedural Dataflow Analysis via Graph Reachability. In Princ. of Prog. Lang. (POPL'95). T. Reps S. Horwitz and M. Sagiv. 1995. Precise Interprocedural Dataflow Analysis via Graph Reachability. In Princ. of Prog. Lang. (POPL'95) .","DOI":"10.1145\/199448.199462"},{"key":"e_1_3_2_2_78_1","doi-asserted-by":"crossref","unstructured":"M. Sagiv T. Reps and S. Horwitz. 1996. Precise Interprocedural Dataflow Analysis with Applications to Constant Propagation. Theor. Comp. Sci. 167 (1996). Issue 1. M. Sagiv T. Reps and S. Horwitz. 1996. Precise Interprocedural Dataflow Analysis with Applications to Constant Propagation. Theor. Comp. Sci. 167 (1996). Issue 1.","DOI":"10.1016\/0304-3975(96)00072-2"},{"key":"e_1_3_2_2_79_1","doi-asserted-by":"crossref","unstructured":"S. Sankaranarayanan A. Chakarov and S. Gulwani. 2013. Static Analysis for Probabilistic Programs: Inferring Whole Program Properties from Finitely Many Paths. In Prog. Lang. Design and Impl. (PLDI'13). S. Sankaranarayanan A. Chakarov and S. Gulwani. 2013. Static Analysis for Probabilistic Programs: Inferring Whole Program Properties from Finitely Many Paths. In Prog. Lang. Design and Impl. (PLDI'13) .","DOI":"10.1145\/2491956.2462179"},{"key":"e_1_3_2_2_80_1","unstructured":"M. Sharir and A. Pnueli. 1981. Two Approaches to Interprocedural Data Flow Analysis. In Program Flow Analysis: Theory and Applications. Prentice-Hall. M. Sharir and A. Pnueli. 1981. Two Approaches to Interprocedural Data Flow Analysis. In Program Flow Analysis: Theory and Applications . Prentice-Hall."},{"key":"e_1_3_2_2_81_1","volume-title":"A Unified Approach to Path Problems. J. ACM 28 (July","author":"Tarjan R. E.","year":"1981","unstructured":"R. E. Tarjan . 1981. A Unified Approach to Path Problems. J. ACM 28 (July 1981 ). Issue 3. R. E. Tarjan. 1981. A Unified Approach to Path Problems. J. ACM 28 (July 1981). Issue 3."},{"key":"e_1_3_2_2_82_1","doi-asserted-by":"crossref","unstructured":"R. Tix K. Keimel and G. Plotkin. 2009. Semantic Domains for Combining Probability and Non-Determinism. Electr. Notes Theor. Comp. Sci. 222 (February 2009). R. Tix K. Keimel and G. Plotkin. 2009. Semantic Domains for Combining Probability and Non-Determinism. Electr. Notes Theor. Comp. Sci. 222 (February 2009).","DOI":"10.1016\/j.entcs.2009.01.002"},{"key":"e_1_3_2_2_83_1","unstructured":"D. Wang J. Hoffmann and T. Reps. 2018. A Denotational Semantics for Nondeterminism in Probabilistic Programs. Available at www.cs.cmu.edu\/~diw3\/papers\/WangHR18.pdf. D. Wang J. Hoffmann and T. Reps. 2018. A Denotational Semantics for Nondeterminism in Probabilistic Programs. Available at www.cs.cmu.edu\/~diw3\/papers\/WangHR18.pdf."},{"key":"e_1_3_2_2_84_1","unstructured":"D. Wojtczak and K. Etessami. 2017. PReMo s Probabilistic Recursive Models analyzer. Available at groups.inf.ed.ac.uk\/premo\/. D. Wojtczak and K. Etessami. 2017. PReMo s Probabilistic Recursive Models analyzer. Available at groups.inf.ed.ac.uk\/premo\/."}],"event":{"name":"PLDI '18: ACM SIGPLAN Conference on Programming Language Design and Implementation","location":"Philadelphia PA USA","acronym":"PLDI '18","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3192366.3192408","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3192366.3192408","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:07:53Z","timestamp":1750198073000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3192366.3192408"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,6,11]]},"references-count":82,"alternative-id":["10.1145\/3192366.3192408","10.1145\/3192366"],"URL":"https:\/\/doi.org\/10.1145\/3192366.3192408","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/3296979.3192408","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2018,6,11]]},"assertion":[{"value":"2018-06-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}