{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:11:55Z","timestamp":1775873515568,"version":"3.50.1"},"reference-count":92,"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\/"}],"funder":[{"name":"European Research Council","award":["863818 (ForM-SMArt)"],"award-info":[{"award-number":["863818 (ForM-SMArt)"]}]},{"name":"Hong Kong Research Grants Council","award":["26208122"],"award-info":[{"award-number":["26208122"]}]}],"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>\n            Cost analysis, also known as resource usage analysis, is the task of finding bounds on the total cost of a program and is a well-studied problem in static analysis. In this work, we consider two classical quantitative problems in cost analysis for probabilistic programs. The first problem is to find a bound on the expected total cost of the program. This is a natural measure for the resource usage of the program and can also be directly applied to average-case runtime analysis. The second problem asks for a tail bound, i.e.\u2004\u200dgiven a threshold\n            <jats:italic>t<\/jats:italic>\n            the goal is to find a probability bound\n            <jats:italic>p<\/jats:italic>\n            such that \u2119[total cost \u2265\n            <jats:italic>t<\/jats:italic>\n            ] \u2264\n            <jats:italic>p<\/jats:italic>\n            . Intuitively, given a threshold\n            <jats:italic>t<\/jats:italic>\n            on the resource, the problem is to find the likelihood that the total cost exceeds this threshold.\n          <\/jats:p>\n          <jats:p>First, for expectation bounds, a major obstacle in previous works on cost analysis is that they can handle only non-negative costs or bounded variable updates. In contrast, we provide a new variant of the standard notion of cost martingales, that allows us to find expectation bounds for a class of programs with general positive or negative costs and no restriction on the variable updates. More specifically, our approach is applicable as long as there is a lower bound on the total cost incurred along every path.<\/jats:p>\n          <jats:p>Second, for tail bounds, all previous methods are limited to programs in which the expected total cost is finite. In contrast, we present a novel approach, based on a combination of our martingale-based method for expectation bounds with a quantitative safety analysis, to obtain a solution to the tail bound problem that is applicable even to programs with infinite expected cost. Specifically, this allows us to obtain runtime tail bounds for programs that do not terminate almost-surely.<\/jats:p>\n          <jats:p>In summary, we provide a novel combination of martingale-based cost analysis and quantitative safety analysis that is able to find expectation and tail cost bounds for probabilistic programs, without the restrictions of non-negative costs, bounded updates, or finiteness of the expected total cost. Finally, we provide experimental results showcasing that our approach can solve instances that were beyond the reach of previous methods.<\/jats:p>","DOI":"10.1145\/3649824","type":"journal-article","created":{"date-parts":[[2024,4,29]],"date-time":"2024-04-29T17:53:50Z","timestamp":1714413230000},"page":"362-391","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":13,"title":["Quantitative Bounds on Resource Usage of Probabilistic Programs"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4561-241X","authenticated-orcid":false,"given":"Krishnendu","family":"Chatterjee","sequence":"first","affiliation":[{"name":"IST Austria, Klosterneuburg, Austria"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1702-6584","authenticated-orcid":false,"given":"Amir Kafshdar","family":"Goharshady","sequence":"additional","affiliation":[{"name":"Hong Kong University of Science and Technology, Hong Kong, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1712-2165","authenticated-orcid":false,"given":"Tobias","family":"Meggendorfer","sequence":"additional","affiliation":[{"name":"Lancaster University Leipzig, Leipzig, Germany"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4681-1699","authenticated-orcid":false,"given":"\u0110or\u0111e","family":"\u017dikeli\u0107","sequence":"additional","affiliation":[{"name":"Singapore Management University, Singapore, Singapore"}]}],"member":"320","published-online":{"date-parts":[[2024,4,29]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81688-9_1"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158122"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434333"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15769-1_8"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454076"},{"key":"e_1_2_1_6_1","doi-asserted-by":"crossref","first-page":"152","DOI":"10.1080\/00029890.2004.11920059","article-title":"Solving inequalities and proving Farkas\u2019s lemma made easy","volume":"111","author":"Avis David","year":"2004","unstructured":"David Avis and Bohdan Kaluzny. 2004. Solving inequalities and proving Farkas\u2019s lemma made easy. The American Mathematical Monthly, 111, 2 (2004), 152\u2013157.","journal-title":"The American Mathematical Monthly"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/TIFS.2016.2623588"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_5"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480894"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-31784-3_15"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_7"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434320"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523721"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454111"},{"key":"e_1_2_1_15_1","article-title":"Pyro: Deep Universal Probabilistic Programming","volume":"20","author":"Bingham Eli","year":"2019","unstructured":"Eli Bingham, Jonathan P. Chen, Martin Jankowiak, Fritz Obermeyer, Neeraj Pradhan, Theofanis Karaletsos, Rohit Singh, Paul A. Szerlip, Paul Horsfall, and Noah D. Goodman. 2019. Pyro: Deep Universal Probabilistic Programming. J. Mach. Learn. Res., 20 (2019), 28:1\u201328:6. http:\/\/jmlr.org\/papers\/v20\/18-403.html","journal-title":"J. Mach. Learn. Res."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737955"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_34"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41528-4_1"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385969"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3174800"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-13185-1_4"},{"key":"e_1_2_1_22_1","volume-title":"Tobias Meggendorfer, and \u0110 or\u0111 e \u017dikeli\u0107.","author":"Chatterjee Krishnendu","year":"2024","unstructured":"Krishnendu Chatterjee, Amir Kafshdar Goharshady, Tobias Meggendorfer, and \u0110 or\u0111 e \u017dikeli\u0107. 2024. Quantitative Bounds on Resource Usage of Probabilistic Programs. https:\/\/hal.science\/hal-04491689"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454093"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3585391"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","unstructured":"Krishnendu Chatterjee Petr Novotn\u00fd and \u0110 or\u0111 e \u017dikeli\u0107. 2017. Stochastic Invariants for Probabilistic Termination. In POPL. 145\u2013160. https:\/\/doi.org\/10.1145\/3009837.3009873 10.1145\/3009837.3009873","DOI":"10.1145\/3009837.3009873"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","unstructured":"Jianhui Chen and Fei He. 2020. Proving almost-sure termination by omega-regular decomposition. In PLDI. 869\u2013882. https:\/\/doi.org\/10.1145\/3385412.3386002 10.1145\/3385412.3386002","DOI":"10.1145\/3385412.3386002"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009858"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314603"},{"key":"e_1_2_1_29_1","volume-title":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 93\u2013107","author":"Cimatti Alessandro","year":"2013","unstructured":"Alessandro Cimatti, Alberto Griggio, Bastiaan Joost Schaafsma, and Roberto Sebastiani. 2013. The mathsat5 smt solver. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 93\u2013107."},{"key":"e_1_2_1_30_1","doi-asserted-by":"crossref","unstructured":"GE Collins. 1982. Quantifier elimination for real closed fields: a guide to the literature. Computer Algebra 79\u201381.","DOI":"10.1007\/978-3-7091-3406-1_6"},{"key":"e_1_2_1_31_1","volume-title":"Beigepaper: an ethereum technical specification","author":"Dameron Micah","unstructured":"Micah Dameron. 2018. Beigepaper: an ethereum technical specification. Ethereum Foundation."},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1515\/crll.1902.124.1"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2010.09.014"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(84)80039-X"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677001"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","unstructured":"Hongfei Fu and Krishnendu Chatterjee. 2019. Termination of Nondeterministic Probabilistic Programs. In VMCAI. 468\u2013490. https:\/\/doi.org\/10.1007\/978-3-030-11245-5_22 10.1007\/978-3-030-11245-5_22","DOI":"10.1007\/978-3-030-11245-5_22"},{"key":"e_1_2_1_37_1","volume-title":"SMT Workshop","author":"Gario Marco","year":"2015","unstructured":"Marco Gario and Andrea Micheli. 2015. PySMT: a solver-agnostic library for fast prototyping of SMT-based algorithms. In SMT Workshop 2015."},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41528-4_4"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1038\/nature14541"},{"key":"e_1_2_1_40_1","volume-title":"Algorand: Scaling Byzantine Agreements for Cryptocurrencies. In SOSP. 51\u201368.","author":"Gilad Yossi","year":"2017","unstructured":"Yossi Gilad, Rotem Hemo, Silvio Micali, Georgios Vlachos, and Nickolai Zeldovich. 2017. Algorand: Scaling Byzantine Agreements for Cryptocurrencies. In SOSP. 51\u201368."},{"key":"e_1_2_1_41_1","unstructured":"Noah D Goodman Vikash K Mansinghka Daniel Roy Keith Bonawitz and Joshua B Tenenbaum. 2008. Church: a language for generative models. In UAI. 220\u2013229."},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/2593882.2593900"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480898"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806596.1806630"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.future.2019.03.002"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.2140\/pjm.1988.132.35"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/2362389.2362393"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_64"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009842"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11957-6_16"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360555"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-16(4:3)2020"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3208102"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","unstructured":"Andrew Kenyon-Roberts and C.-H. Luke Ong. 2021. Supermartingales Ranking Functions and Probabilistic Lambda Calculus. In LICS. 1\u201313. https:\/\/doi.org\/10.1109\/LICS52264.2021.9470550 10.1109\/LICS52264.2021.9470550","DOI":"10.1109\/LICS52264.2021.9470550"},{"key":"e_1_2_1_55_1","volume-title":"Ouroboros: A Provably Secure Proof-of-Stake Blockchain Protocol. In CRYPTO (1) (Lecture Notes in Computer Science","author":"Kiayias Aggelos","year":"2017","unstructured":"Aggelos Kiayias, Alexander Russell, Bernardo David, and Roman Oliynykov. 2017. Ouroboros: A Provably Secure Proof-of-Stake Blockchain Protocol. In CRYPTO (1) (Lecture Notes in Computer Science, Vol. 10401). Springer, 357\u2013388."},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062373"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(81)90036-2"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17465-1_8"},{"key":"e_1_2_1_59_1","volume-title":"Rosenschein","author":"Lewenberg Yoad","year":"2015","unstructured":"Yoad Lewenberg, Yoram Bachrach, Yonatan Sompolinsky, Aviv Zohar, and Jeffrey S. Rosenschein. 2015. Bitcoin Mining Pools: A Cooperative Game Theoretic Analysis. In AAMAS. 919\u2013927."},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1007\/11889229_4"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1007\/b138392"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158121"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","unstructured":"Tobias Meggendorfer and \u0110or\u0111e \u017dikeli\u0107. 2024. Artefact for: Quantitative Bounds on Resource Usage of Probabilistic Programs. https:\/\/doi.org\/10.5281\/zenodo.10457566 10.5281\/zenodo.10457566","DOI":"10.5281\/zenodo.10457566"},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.7717\/peerj-cs.103"},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","unstructured":"David Monniaux. 2001. An Abstract Analysis of the Probabilistic Termination of Programs. In SAS. 111\u2013126. https:\/\/doi.org\/10.1007\/3-540-47764-0_7 10.1007\/3-540-47764-0_7","DOI":"10.1007\/3-540-47764-0_7"},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72019-3_18"},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74407-8_28"},{"key":"e_1_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00596-1_26"},{"key":"e_1_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192394"},{"key":"e_1_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/3156018"},{"key":"e_1_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2935317"},{"key":"e_1_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.1512\/iumj.1993.42.42045"},{"key":"e_1_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341696"},{"key":"e_1_2_1_75_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158124"},{"key":"e_1_2_1_76_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(10)80005-7"},{"key":"e_1_2_1_77_1","first-page":"26","article-title":"A stochastic programming perspective on nonparametric Bayes","volume":"22","author":"Roy DM","year":"2008","unstructured":"DM Roy, VK Mansinghka, ND Goodman, and JB Tenenbaum. 2008. A stochastic programming perspective on nonparametric Bayes. In ICML. 22, 26.","journal-title":"ICML."},{"key":"e_1_2_1_78_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27864-1_7"},{"key":"e_1_2_1_79_1","unstructured":"Erez Shinan. 2023. Lark - a parsing toolkit for Python. https:\/\/github.com\/lark-parser\/lark\/"},{"key":"e_1_2_1_80_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_50"},{"key":"e_1_2_1_81_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-016-9402-4"},{"key":"e_1_2_1_82_1","doi-asserted-by":"publisher","DOI":"10.1145\/3450967"},{"key":"e_1_2_1_83_1","doi-asserted-by":"publisher","DOI":"10.1609\/aimag.v21i4.1534"},{"key":"e_1_2_1_84_1","doi-asserted-by":"publisher","DOI":"10.1145\/3064899.3064910"},{"key":"e_1_2_1_85_1","volume-title":"An Introduction to Probabilistic Programming. CoRR, abs\/1809.10756","author":"van de Meent Jan-Willem","year":"2018","unstructured":"Jan-Willem van de Meent, Brooks Paige, Hongseok Yang, and Frank Wood. 2018. An Introduction to Probabilistic Programming. CoRR, abs\/1809.10756 (2018), arXiv:1809.10756. arxiv:1809.10756"},{"key":"e_1_2_1_86_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523435"},{"key":"e_1_2_1_87_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454062"},{"key":"e_1_2_1_88_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408992"},{"key":"e_1_2_1_89_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371093"},{"key":"e_1_2_1_90_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314581"},{"key":"e_1_2_1_91_1","volume-title":"Probability with Martingales","author":"Williams D.","unstructured":"D. Williams. 1991. Probability with Martingales. Cambridge University Press, Cambridge, UK."},{"key":"e_1_2_1_92_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-23702-7_22"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3649824","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3649824","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\/3649824"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,4,29]]},"references-count":92,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2024,4,29]]}},"alternative-id":["10.1145\/3649824"],"URL":"https:\/\/doi.org\/10.1145\/3649824","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"}}]}}