{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T11:05:43Z","timestamp":1784199943838,"version":"3.55.0"},"reference-count":58,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","funder":[{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["62072267, 62021002"],"award-info":[{"award-number":["62072267, 62021002"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,10,9]]},"abstract":"<jats:p>\n                    In this paper, we present structural abstraction refinement, a novel framework for verifying the threshold problem of probabilistic programs. Our approach represents the structure of a Probabilistic Control-Flow Automaton (PCFA) as a Markov Decision Process (MDP) by abstracting away statement semantics. The maximum reachability of the MDP naturally provides a proper upper bound of the violation probability, termed the\n                    <jats:italic toggle=\"yes\">structural upper bound<\/jats:italic>\n                    . This introduces a fresh \u201cstructural\u201d characterization of the relationship between PCFA and MDP, contrasting with the traditional \u201csemantical\u201d view, where the MDP reflects semantics. The method uniquely features a clean separation of concerns between probability and computational semantics that the abstraction focuses solely on probabilistic computation and the refinement handles only the semantics aspect, where the latter allows non-random program verification techniques to be employed without modification.\n                  <\/jats:p>\n                  <jats:p>Building upon this feature, we propose a general counterexample-guided abstraction refinement (CEGAR) framework, capable of leveraging established non-probabilistic techniques for probabilistic verification. We explore its instantiations using trace abstraction. Our method was evaluated on a diverse set of examples against state-of-the-art tools, and the experimental results highlight its versatility and ability to handle more flexible structures swiftly.<\/jats:p>","DOI":"10.1145\/3763115","type":"journal-article","created":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T08:49:50Z","timestamp":1759999790000},"page":"1809-1836","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Structural Abstraction and Refinement for Probabilistic Programs"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4163-1840","authenticated-orcid":false,"given":"Guanyan","family":"Li","sequence":"first","affiliation":[{"name":"Tsinghua University, Beijing, China"},{"name":"University of Oxford, Oxford, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-6791-6466","authenticated-orcid":false,"given":"Juanen","family":"Li","sequence":"additional","affiliation":[{"name":"Beijing Normal University, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9171-4997","authenticated-orcid":false,"given":"Zhilei","family":"Han","sequence":"additional","affiliation":[{"name":"Tsinghua University, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3241-0023","authenticated-orcid":false,"given":"Peixin","family":"Wang","sequence":"additional","affiliation":[{"name":"East China Normal University, Shanghai, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7947-3446","authenticated-orcid":false,"given":"Hongfei","family":"Fu","sequence":"additional","affiliation":[{"name":"Shanghai Jiao Tong University, Shanghai, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4266-875X","authenticated-orcid":false,"given":"Fei","family":"He","sequence":"additional","affiliation":[{"name":"Tsinghua University, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,10,9]]},"reference":[{"key":"e_1_3_1_2_2","volume-title":"Principles of model checking","author":"Baier Christel","year":"2008","unstructured":"Christel Baier and Joost-Pieter Katoen. 2008. Principles of model checking. MIT press."},{"key":"e_1_3_1_3_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-13185-1_3"},{"key":"e_1_3_1_4_2","unstructured":"Gilles Barthe Marco Gaboardi Benjamin Gr\u00e9goire Justin Hsu andPierre-Yves Strub. 2016. A program logic for union bounds. arXiv preprint arXiv:1602.05681 (2016)."},{"key":"e_1_3_1_5_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-31784-3_15"},{"key":"e_1_3_1_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-30820-8_25"},{"key":"e_1_3_1_7_2","doi-asserted-by":"crossref","unstructured":"Raven Beutner C-H Luke Ong andFabian Zaiser. 2022. Guaranteed bounds for posterior inference in universal probabilistic programming. In Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation. 536-551.","DOI":"10.1145\/3519939.3523721"},{"key":"e_1_3_1_8_2","first-page":"1","author":"Bj\u00f8rner Nikolaj S","year":"2014","unstructured":"Nikolaj S Bj\u00f8rner andAnh-Dung Phan. 2014. vZ-Maximal Satisfaction with Z3. Scss 30(2014), 1-9.","journal-title":"vZ-Maximal Satisfaction with Z3"},{"key":"e_1_3_1_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/2544173.2509546"},{"issue":"1","key":"e_1_3_1_10_2","first-page":"1","volume":"76","author":"Carpenter Bob","year":"2017","unstructured":"Bob Carpenter, Andrew Gelman, Matthew D Hoffman, Daniel Lee, Ben Goodrich, Michael Betancourt, Marcus Brubaker, Jiqiang Guo, Peter Li, and Allen Riddell. 2017. Stan: A probabilistic programming language. Journal of statistical software 76, 1 (2017), 1-32.","journal-title":"Journal of statistical software"},{"key":"e_1_3_1_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_34"},{"key":"e_1_3_1_12_2","unstructured":"Anne Chao. 1984. Nonparametric estimation of the number of classes in a population. Scandinavian fournal of statistics (1984) 265-270."},{"key":"e_1_3_1_13_2","doi-asserted-by":"crossref","unstructured":"Jianhui Chen and Fei He. 2020. Proving almost-sure termination by omega-regular decomposition. In Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation. 869-882.","DOI":"10.1145\/3385412.3386002"},{"key":"e_1_3_1_14_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31759-0_19"},{"key":"e_1_3_1_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_15"},{"key":"e_1_3_1_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"issue":"8","key":"e_1_3_1_17_2","first-page":"453","volume":"18","author":"Dijkstra Edsger W","year":"1975","unstructured":"Edsger W Dijkstra. 1975. Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM 18, 8 (1975), 453-457.","journal-title":"Commun"},{"key":"e_1_3_1_18_2","unstructured":"M. Duflot M. Kwiatkowska G. Norman and D. Parker. 2004. A Formal Analysis of Bluetooth Device Discovery. In Proc. 1st International Symposium on Leveraging Applications of Formal Methods (ISOLA\u201904)."},{"key":"e_1_3_1_19_2","doi-asserted-by":"publisher","DOI":"10.1007\/11681878_14"},{"key":"e_1_3_1_20_2","unstructured":"P\u00e1l Erd\u0151s and Alfr\u00e9d R\u00e9nyi. 1961. On a classical problem of probability theory. A Magyar Tudom\u00e1nyos Akad\u00e9mia Matematikai Kutat\u00f3 Int\u00e9zet\u00e9nek K\u00f6zlem\u00e9nyei 6 1-2 (1961) 215-220."},{"key":"e_1_3_1_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41528-4_4"},{"key":"e_1_3_1_22_2","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(84)90070-9"},{"key":"e_1_3_1_23_2","unstructured":"Noah Goodman Vikash Mansinghka Daniel M Roy Keith Bonawitz and Joshua B Tenenbaum. 2012. Church: a language for generative models. arXiv preprint arXiv:1206.3255 (2012)."},{"key":"e_1_3_1_24_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.peva.2013.11.004"},{"key":"e_1_3_1_25_2","unstructured":"David Hall Daniel Ramage Jason Zaugg Alexander Lehmann Jonathan Merritt Keith Stevens Jason Baldridge Timothy Hunter Dave DeCaprio Daniel Duckworth et al. 2009. ScalaNLP:Breeze. https:\/\/github.com\/scalanlp\/breeze"},{"issue":"2","key":"e_1_3_1_26_2","doi-asserted-by":"crossref","first-page":"241","DOI":"10.1109\/TSE.2009.5","article-title":"Counterexample generation in probabilistic model checking","volume":"35","author":"Han Tingting","year":"2009","unstructured":"Tingting Han, Joost-Pieter Katoen, and Damman Berteun. 2009. Counterexample generation in probabilistic model checking. IEEE transactions on software engineering 35, 2 (2009), 241-257.","journal-title":"IEEE transactions on software engineering"},{"key":"e_1_3_1_27_2","doi-asserted-by":"crossref","unstructured":"J. Heath M. Kwiatkowska G. Norman D. Parker and O. Tymchyshyn. 2008. Probabilistic model checking of complex biological pathways. Theoretical Computer Science 319 3 (2008) 239-257.","DOI":"10.1016\/j.tcs.2007.11.013"},{"key":"e_1_3_1_28_2","unstructured":"Matthias Heizmann. [n.d.]. Uni-Freiburg:SWT-Ultimate. https:\/\/monteverdi.informatik.uni-freiburg.de\/tomcat\/Website\/?ui=tool&tool=automizer November 02 2021."},{"key":"e_1_3_1_29_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03237-0_7"},{"key":"e_1_3_1_30_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_53"},{"key":"e_1_3_1_31_2","unstructured":"Christian Hensel Sebastian Junges Joost-Pieter Katoen Tim Quatmann and Matthias Volk. 2022. The probabilistic model checker Storm. International Fournal on Software Tools for Technology Transfer (2022) 1-22."},{"key":"e_1_3_1_32_2","doi-asserted-by":"crossref","unstructured":"Thomas A Henzinger Ranjit Jhala Rupak Majumdar and Kenneth L McMillan. 2004. Abstractions from proofs. In Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages. 232-244.","DOI":"10.1145\/964001.964021"},{"key":"e_1_3_1_33_2","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(90)90107-9"},{"key":"e_1_3_1_34_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_16"},{"issue":"10","key":"e_1_3_1_35_2","first-page":"576","volume":"12","author":"Hoare Charles Antony Richard","year":"1969","unstructured":"Charles Antony Richard Hoare. 1969. An axiomatic basis for computer programming. Commun. ACM 12, 10 (1969), 576-580.","journal-title":"Commun"},{"key":"e_1_3_1_36_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-46520-3_5"},{"key":"e_1_3_1_37_2","doi-asserted-by":"publisher","DOI":"10.1162\/COLI_a_00136"},{"key":"e_1_3_1_38_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46029-2_13"},{"key":"e_1_3_1_39_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-012-0227-6"},{"key":"e_1_3_1_40_2","doi-asserted-by":"crossref","unstructured":"Marta Kwiatkowska Gethin Norman and David Parker. 2018. Probabilistic model checking: Advances and applications. Formal System Verification: State-of the-Art and Future Trends (2018) 73-121.","DOI":"10.1007\/978-3-319-57685-5_3"},{"key":"e_1_3_1_41_2","doi-asserted-by":"publisher","unstructured":"Guanyan Li Juanen Li Zhilei Han Peixin Wang Hongfei Fu andFei He. 2025. Artifact of OOPSLA Paper: Structural Abstraction and Refinement for Probabilistic Programs. Zenodo. https:\/\/doi.org\/10.5281\/zenodo.15760713 10.5281\/zenodo.15760713","DOI":"10.5281\/zenodo.15760713"},{"key":"e_1_3_1_42_2","volume-title":"Abstraction, refinement and proof for probabilistic systems","author":"McIver Annabelle","year":"2005","unstructured":"Annabelle McIver, Carroll Morgan, andCharles Carroll Morgan. 2005. Abstraction, refinement and proof for probabilistic systems. Springer Science & Business Media."},{"key":"e_1_3_1_43_2","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_14"},{"key":"e_1_3_1_44_2","volume-title":"Probability and computing: Randomization and probabilistic techniques in algorithms and data analysis","author":"Mitzenmacher Michael","year":"2017","unstructured":"Michael Mitzenmacher and Eli Upfal. 2017. Probability and computing: Randomization and probabilistic techniques in algorithms and data analysis. Cambridge university press."},{"key":"e_1_3_1_45_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-90870-6_36"},{"key":"e_1_3_1_46_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511814075"},{"key":"e_1_3_1_47_2","unstructured":"Anders M\u00f8ller. 2012. dk.brics.automaton. https:\/\/www.brics.dk\/automaton\/"},{"key":"e_1_3_1_48_2","unstructured":"G. Norman D. Parker M. Kwiatkowska S. Shukla and R. Gupta. 2003. Using Probabilistic Model Checking for Dynamic Power Management. In Proc. 3rd Workshop on Automated Verification of Critical Systems (AVoCS\u201903) (Technical Report DSSE-TR-2003-2 University of Southampton) M. Leuschel S. Gruner and S. Lo Presti(Eds.).202-215."},{"key":"e_1_3_1_49_2","unstructured":"Benjamin C. Pierce Arthur Azevedo de Amorim Chris Casinghino Marco Gaboardi Michael Greenberg C\u0103t\u0103lin Hri\u0163cu Vilhelm Sj\u00f6berg and Brent Yorgey. 2022. Logical Foundations. Software Foundations Vol.1. Electronic textbook."},{"key":"e_1_3_1_50_2","volume-title":"Probabilistic Algorithms Algorithms and Complexity: New Directions and Recent Results","author":"Rabin Michael O","year":"1976","unstructured":"Michael O Rabin. 1976. Probabilistic Algorithms Algorithms and Complexity: New Directions and Recent Results. Academic PressNew York."},{"key":"e_1_3_1_51_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-99725-4_22"},{"key":"e_1_3_1_52_2","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462179"},{"key":"e_1_3_1_53_2","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9939-1969-0249221-4"},{"issue":"2019","key":"e_1_3_1_54_2","first-page":"1","volume":"3","author":"Smith Calvin","year":"2019","unstructured":"Calvin Smith, Justin Hsu, and Aws Albarghouthi. 2019. Trace abstraction modulo probability. Proceedings of the ACM on Programming Languages 3, POPL (2019), 1-31.","journal-title":"Proceedings of the ACM on Programming Languages"},{"key":"e_1_3_1_55_2","doi-asserted-by":"crossref","unstructured":"David Tolpin Jan Willem van de Meent Hongseok Yang and Frank Wood. 2016. Design and Implementation of Probabilistic Programming Language Anglican. arXiv preprint arXiv:1608.05263(2016).","DOI":"10.1145\/3064899.3064910"},{"key":"e_1_3_1_56_2","doi-asserted-by":"crossref","unstructured":"Jinyi Wang Yican Sun Hongfei Fu Krishnendu Chatterjee andAmir Kafshdar Goharshady. 2021. Quantitative analysis of assertion violations in probabilistic programs. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation. 1171-1186.","DOI":"10.1145\/3453483.3454102"},{"key":"e_1_3_1_57_2","doi-asserted-by":"publisher","DOI":"10.1145\/3656432"},{"key":"e_1_3_1_58_2","doi-asserted-by":"publisher","DOI":"10.14257\/ijmue.2016.11.3.18"},{"key":"e_1_3_1_59_2","doi-asserted-by":"publisher","DOI":"10.1145\/3704874"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3763115","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T10:06:24Z","timestamp":1784196384000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3763115"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,9]]},"references-count":58,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2025,10,9]]}},"alternative-id":["10.1145\/3763115"],"URL":"https:\/\/doi.org\/10.1145\/3763115","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,10,9]]},"assertion":[{"value":"2025-03-26","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-08-12","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-10-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}