{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,21]],"date-time":"2026-07-21T23:04:03Z","timestamp":1784675043539,"version":"3.55.0"},"reference-count":70,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA1","license":[{"start":{"date-parts":[[2024,4,29]],"date-time":"2024-04-29T00:00:00Z","timestamp":1714348800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,4,29]]},"abstract":"<jats:p>Due to their quantitative nature, probabilistic programs pose non-trivial challenges for designing compositional and efficient program analyses. Many analyses for probabilistic programs rely on iterative approximation. This article presents an interprocedural dataflow-analysis framework, called NPA-PMA, for designing and implementing (partially) non-iterative program analyses of probabilistic programs with unstructured control-flow, nondeterminism, and general recursion. NPA-PMA is based on Newtonian Program Analysis (NPA), a generalization of Newton's method to solve equation systems over semirings. The key challenge for developing NPA-PMA is to handle multiple kinds of confluences in both the algebraic structures that specify analyses and the equation systems that encode control flow: semirings support a single confluence operation, whereas NPA-PMA involves three confluence operations (conditional, probabilistic, and nondeterministic).<\/jats:p>\n          <jats:p>Our work introduces \u03c9-continuous pre-Markov algebras (\u03c9PMAs) to factor out common parts of different analyses; adopts regular infinite-tree expressions to encode probabilistic programs with unstructured control-flow; and presents a linearization method that makes Newton's method applicable to the setting of regular-infinite-tree equations over \u03c9PMAs. NPA-PMA allows analyses to supply a non-iterative strategy to solve linearized equations. Our experimental evaluation demonstrates that (i) NPA-PMA holds considerable promise for outperforming Kleene iteration, and (ii) provides great generality for designing program analyses.<\/jats:p>","DOI":"10.1145\/3649822","type":"journal-article","created":{"date-parts":[[2024,4,29]],"date-time":"2024-04-29T17:53:50Z","timestamp":1714413230000},"page":"305-333","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Newtonian Program Analysis of Probabilistic Programs"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2418-7987","authenticated-orcid":false,"given":"Di","family":"Wang","sequence":"first","affiliation":[{"name":"Peking University, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5676-9949","authenticated-orcid":false,"given":"Thomas","family":"Reps","sequence":"additional","affiliation":[{"name":"University of Wisconsin, Madison, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,4,29]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428240"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","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 (1997) April https:\/\/doi.org\/10.1023\/A:1008699807402 10.1023\/A:1008699807402","DOI":"10.1023\/A:1008699807402"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41528-4_3"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","unstructured":"Ezio Bartocci Laura Kov\u00e1cs and Miroslav Stankovi\u010d. 2019. Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops. In Automated Tech. for Verif. and Analysis (ATVA\u201919). https:\/\/doi.org\/10.1007\/978-3-030-31784-3_15 10.1007\/978-3-030-31784-3_15","DOI":"10.1007\/978-3-030-31784-3_15"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0048939"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","unstructured":"Ahmed Bouajjani Javier Esparza and Tayssir Touili. 2003. A Generic Approach to the Static Analysis of Concurrent Programs with Procedures. In Princ. of Prog. Lang. (POPL\u201903). https:\/\/doi.org\/10.1145\/604131.604137 10.1145\/604131.604137","DOI":"10.1145\/604131.604137"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","unstructured":"Olivier Bouissou Eric Goubault Sylvie Putot Aleksandar Chakarov and Sriram Sankaranarayanan. 2016. Uncertainty Propagation Using Probabilistic Affine Forms and Concentration of Measure Inequalities. In Tools and Algs. for the Construct. and Anal. of Syst. (TACAS\u201916). https:\/\/doi.org\/10.1007\/978-3-662-49674-9_13 10.1007\/978-3-662-49674-9_13","DOI":"10.1007\/978-3-662-49674-9_13"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","unstructured":"Tom\u00e1 Br\u00e1zdil Stefan Kiefer and Anton\u00edn Ku\u010dera. 2011. Efficient Analysis of Probabilistic Programs with an Unbounded Counter. In Computer Aided Verif. (CAV\u201911). 208\u2013224. https:\/\/doi.org\/10.1007\/978-3-642-22110-1_18 10.1007\/978-3-642-22110-1_18","DOI":"10.1007\/978-3-642-22110-1_18"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","unstructured":"Jason Breck John Cyphert Zachary Kincaid and Thomas Reps. 2020. Templates and Recurrences: Better Together. In Prog. Lang. Design and Impl. (PLDI\u201920). 688\u2013702. https:\/\/doi.org\/10.1145\/3385412.3386035 10.1145\/3385412.3386035","DOI":"10.1145\/3385412.3386035"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","unstructured":"Quentin Carbonneaux Jan Hoffmann Thomas Reps and Zhong Shao. 2017. Automated Resource Analysis with Coq Proof Objects. In Computer Aided Verif. (CAV\u201917). https:\/\/doi.org\/10.1007\/978-3-319-63390-9_4 10.1007\/978-3-319-63390-9_4","DOI":"10.1007\/978-3-319-63390-9_4"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","unstructured":"Aleksandar Chakarov and Sriram Sankaranarayanan. 2013. Probabilistic Program Analysis with Martingales. In Computer Aided Verif. (CAV\u201913). 511\u2013526. https:\/\/doi.org\/10.1007\/978-3-642-39799-8_34 10.1007\/978-3-642-39799-8_34","DOI":"10.1007\/978-3-642-39799-8_34"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10936-7_6"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","unstructured":"Krishnendu Chatterjee Petr Novotn\u00fd and \u00d0or\u0111e \u017dikeli\u0107. 2017. Stochastic Invariants for Probabilistic Termination. In Princ. of Prog. Lang. (POPL\u201917). 145\u2013160. https:\/\/doi.org\/10.1145\/3093333.3009873 10.1145\/3093333.3009873","DOI":"10.1145\/3093333.3009873"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3586050"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","unstructured":"Guillaume Claret Sriram K. Rajamani Aditya V. Nori Andrew D. Gordon and Johannes Borgstr\u00f6m. 2013. Bayesian Inference using Data Flow Analysis. In Found. of Softw. Eng. (FSE\u201913). 92\u2013102. https:\/\/doi.org\/10.1145\/2491411.2491423 10.1145\/2491411.2491423","DOI":"10.1145\/2491411.2491423"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.03.048"},{"key":"e_1_2_1_17_1","unstructured":"Clp team. 2022. COIN-OR Linear Programming Solver. Available on. https:\/\/projects.coin-or.org\/Clp"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(83)90059-2"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/B978-0-444-88074-1.50014-7"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","unstructured":"Patrick Cousot and Radhia Cousot. 1977. Abstract Interpretation: A Unified Latice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In Princ. of Prog. Lang. (POPL\u201977). https:\/\/doi.org\/10.1145\/512950.512973 10.1145\/512950.512973","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28869-2_9"},{"key":"e_1_2_1_22_1","volume-title":"Int. Joint Conf. on Artif. Intelligence (IJCAI\u201907)","author":"Raedt Luc De","year":"2007","unstructured":"Luc De Raedt, Angelika Kimmig, and Hannu Toivonen. 2007. ProbLog: A Probabilistic Prolog and its Application in Link Discovery. In Int. Joint Conf. on Artif. Intelligence (IJCAI\u201907). https:\/\/dl.acm.org\/doi\/10.5555\/1625275.1625673"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","unstructured":"Christian Dehnert Sebastian Junges Joost-Pieter Katoen and Matthias Volk. 2017. A Storm is Coming: A Modern Probabilistic Model Checker. In Computer Aided Verif. (CAV\u201917). https:\/\/doi.org\/10.1007\/978-3-319-63390-9_31 10.1007\/978-3-319-63390-9_31","DOI":"10.1007\/978-3-319-63390-9_31"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511581274"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70575-8_57"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70583-3_2"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1857914.1857917"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","unstructured":"Javier Esparza Anton\u00edn Ku\u010dera and Richard Mayr. 2004. Model Checking Probabilistic Pushdown Automata. In Logic in Computer Science (LICS\u201904). https:\/\/doi.org\/10.1109\/LICS.2004.1319596 10.1109\/LICS.2004.1319596","DOI":"10.1109\/LICS.2004.1319596"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31594-7_27"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-47666-6_15"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31856-9_28"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/11523468_72"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2699431"},{"key":"e_1_2_1_34_1","unstructured":"Azadeh Farzan and Zachary Kincaid. 2013. An Algebraic Framework For Compositional Program Analysis. arxiv:1310.3481"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","unstructured":"Azadeh Farzan and Zachary Kincaid. 2015. Compositional Recurrence Analysis. In Formal Methods in Computer-Aided Design (FMCAD\u201915). https:\/\/doi.org\/10.1109\/FMCAD.2015.7542253 10.1109\/FMCAD.2015.7542253","DOI":"10.1109\/FMCAD.2015.7542253"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33386-6_24"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068414000076"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","unstructured":"Vojt\u011bch Forejt Marta Kwiatkowska Gethin Norman and David Parker. 2011. Automated Verification Techniques for Probabilistic Systems. In Formal Methods for Eternal Networked Software Systems (SFM\u201911). https:\/\/doi.org\/10.1007\/978-3-642-21455-4_3 10.1007\/978-3-642-21455-4_3","DOI":"10.1007\/978-3-642-21455-4_3"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","unstructured":"Susanne Graf and Hassen Saidi. 1997. Construction of Abstract State Graphs with PVS. In Computer Aided Verif. (CAV\u201997). https:\/\/doi.org\/10.1007\/3-540-63166-6_10 10.1007\/3-540-63166-6_10","DOI":"10.1007\/3-540-63166-6_10"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","unstructured":"Ernst Moritz Hahn Holger Hermanns Bj\u00f6rn Wachter and Lijun Zhang. 2010. PASS: Abstraction Refinement for Infinite Probabilistic Models. In Tools and Algs. for the Construct. and Anal. of Syst. (TACAS\u201910). 353\u2013357. https:\/\/doi.org\/10.1007\/978-3-642-12002-2_30 10.1007\/978-3-642-12002-2_30","DOI":"10.1007\/978-3-642-12002-2_30"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","unstructured":"Holger Hermanns Bj\u00f6rn Wachter and Lijun Zhang. 2008. Probabilistic CEGAR. In Computer Aided Verif. (CAV\u201908). 162\u2013175. https:\/\/doi.org\/10.1007\/978-3-540-70545-1_16 10.1007\/978-3-540-70545-1_16","DOI":"10.1007\/978-3-540-70545-1_16"},{"key":"e_1_2_1_42_1","volume-title":"Sound Abstraction and Decomposition of Probabilistic Programs. In Int. Conf. on Machine Learning (ICML\u201918)","author":"Holtzen Steven","year":"2018","unstructured":"Steven Holtzen, Guy Broeck, and Todd Millstein. 2018. Sound Abstraction and Decomposition of Probabilistic Programs. In Int. Conf. on Machine Learning (ICML\u201918). 1999\u20132008."},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428208"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15769-1_24"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","unstructured":"Mark Kattenbelt Marta Kwiatkowska Gethin Norman and David Parker. 2009. Abstraction Refinement for Probabilistic Software. In Verif. Model Checking and Abs. Interp. (VMCAI\u201909). 182\u2013197. https:\/\/doi.org\/10.1007\/978-3-540-93900-9_17 10.1007\/978-3-540-93900-9_17","DOI":"10.1007\/978-3-540-93900-9_17"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062373"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290368"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158142"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","unstructured":"Zachary Kincaid Thomas Reps and John Cyphert. 2021. Algebraic Program Analysis. In Computer Aided Verif. (CAV\u201921). 46\u201383. https:\/\/doi.org\/10.1007\/978-3-030-81685-8_3 10.1007\/978-3-030-81685-8_3","DOI":"10.1007\/978-3-030-81685-8_3"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(81)90036-2"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","unstructured":"Marta Kwiatkowska Gethin Norman and David Parker. 2011. PRISM 4.0: Verification of Probabilistic Real-Time Systems. In Computer Aided Verif. (CAV\u201911). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_47 10.1007\/978-3-642-22110-1_47","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/b138392"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563341"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192394"},{"key":"e_1_2_1_55_1","volume-title":"Infinite Words: Automata, Semigroups, Logic and Games","author":"Pin Jean-Eric","year":"2004","unstructured":"Jean-Eric Pin and Dominique Perrin. 2004. Infinite Words: Automata, Semigroups, Logic and Games. Elsevier."},{"key":"e_1_2_1_56_1","volume-title":"Markov Decision Processes: Discrete Stochastic Dynamic Programming","author":"Puterman Martin L.","unstructured":"Martin L. Puterman. 1994. Markov Decision Processes: Discrete Stochastic Dynamic Programming. John Wiley & Sons, Inc.. https:\/\/dl.acm.org\/doi\/book\/10.5555\/528623"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","unstructured":"Thomas Reps Akash Lal and Nick Kidd. 2007. Program Analysis Using Weighted Pushdown System. In Found. of Soft. Tech. and Theor. Comput. Sci. (FSTTCS\u201907). https:\/\/doi.org\/10.1007\/978-3-540-77050-3_4 10.1007\/978-3-540-77050-3_4","DOI":"10.1007\/978-3-540-77050-3_4"},{"key":"e_1_2_1_58_1","volume-title":"Static Analysis Symp. (SAS\u201903)","author":"Reps Thomas","year":"2003","unstructured":"Thomas Reps, Stefan Schwoon, and Somesh Jha. 2003. Weighted Pushdown Systems and their Application to Interprocedural Dataflow Analysis. In Static Analysis Symp. (SAS\u201903). https:\/\/dl.acm.org\/doi\/10.5555\/1760267.1760283"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","unstructured":"Thomas Reps Emma Turetsky and Prathmesh Prabhu. 2016. Newtonian Program Analysis via Tensor Product. In Princ. of Prog. Lang. (POPL\u201916). 663\u2013677. https:\/\/doi.org\/10.1145\/2837614.2837659 10.1145\/2837614.2837659","DOI":"10.1145\/2837614.2837659"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1017\/S147106841100010X"},{"key":"e_1_2_1_61_1","unstructured":"Anne Schreuder and Luke Ong. 2019. Polynomial Probabilistic Invariants and the Optional Stopping Theorem. arxiv:1910.12634"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/322261.322272"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/322261.322273"},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2009.01.002"},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192408"},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2019.09.016"},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","unstructured":"Di Wang and Thomas Reps. 2023. Newtonian Program Analysis of Probabilistic Programs (Technical Report). https:\/\/doi.org\/10.48550\/arXiv.2307.09064","DOI":"10.48550\/arXiv.2307.09064"},{"key":"e_1_2_1_68_1","doi-asserted-by":"publisher","unstructured":"Di Wang and Thomas Reps. 2024. Newtonian Programs Analysis of Probabilistic Programs (Artifact). https:\/\/doi.org\/10.5281\/zenodo.10791709 10.5281\/zenodo.10791709","DOI":"10.5281\/zenodo.10791709"},{"key":"e_1_2_1_69_1","doi-asserted-by":"publisher","unstructured":"Dominik Wojtczak and Kousha Etessami. 2007. PReMo: An Analyzer for Probabilistic Recursive Models. In Tools and Algs. for the Construct. and Anal. of Syst. (TACAS\u201907). 66\u201371. https:\/\/doi.org\/10.1007\/978-3-540-71209-1_7 10.1007\/978-3-540-71209-1_7","DOI":"10.1007\/978-3-540-71209-1_7"},{"key":"e_1_2_1_70_1","doi-asserted-by":"publisher","unstructured":"Shaowei Zhu and Zachary Kincaid. 2021. Termination Analysis without the Tears. In Prog. Lang. Design and Impl. (PLDI\u201921). https:\/\/doi.org\/10.1145\/3453483.3454110 10.1145\/3453483.3454110","DOI":"10.1145\/3453483.3454110"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3649822","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3649822","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T22:54:06Z","timestamp":1750287246000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3649822"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,4,29]]},"references-count":70,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2024,4,29]]}},"alternative-id":["10.1145\/3649822"],"URL":"https:\/\/doi.org\/10.1145\/3649822","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,4,29]]},"assertion":[{"value":"2024-04-29","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}