{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T14:12:36Z","timestamp":1784211156756,"version":"3.55.0"},"reference-count":59,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T00:00:00Z","timestamp":1767830400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"funder":[{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["62172271"],"award-info":[{"award-number":["62172271"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"crossref","award":["62502475"],"award-info":[{"award-number":["62502475"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"crossref","award":["62192732"],"award-info":[{"award-number":["62192732"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"crossref","award":["W2511064"],"award-info":[{"award-number":["W2511064"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2026,1,8]]},"abstract":"<jats:p>In probabilistic program analysis, quantitative analysis aims at deriving tight numerical bounds for probabilistic properties such as expectation and assertion probability. Most previous works consider numerical bounds over the whole program state space monolithically and do not consider piecewise bounds. Not surprisingly, monolithic bounds are either conservative, or not expressive and succinct enough in general. To derive better bounds, we propose a novel approach for synthesizing piecewise bounds over probabilistic programs. First, we show how to extract useful piecewise information from latticed \ud835\udc58-induction operators, and combine the piecewise information with Optional Stopping Theorem to obtain a general approach to derive piecewise bounds over probabilistic programs. Second, we develop algorithms to synthesize piecewise polynomial bounds, and show that the synthesis can be reduced to bilinear programming in the linear case, and soundly relaxed to semidefinite programming in the polynomial case. Experimental results show that our approach generates tight piecewise bounds for a wide range of benchmarks when compared with the state of the art.<\/jats:p>","DOI":"10.1145\/3776709","type":"journal-article","created":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T18:59:43Z","timestamp":1767898783000},"page":"1933-1963","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Piecewise Analysis of Probabilistic Programs via \ud835\udc58-Induction"],"prefix":"10.1145","volume":"10","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2072-0836","authenticated-orcid":false,"given":"Tengshun","family":"Yang","sequence":"first","affiliation":[{"name":"Institute of Software at Chinese Academy of Sciences, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5352-4954","authenticated-orcid":false,"given":"Shenghua","family":"Feng","sequence":"additional","affiliation":[{"name":"Institute of Software at Chinese Academy of Sciences, Beijing, 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-0003-3298-3817","authenticated-orcid":false,"given":"Naijun","family":"Zhan","sequence":"additional","affiliation":[{"name":"Peking University, Beijing, China"},{"name":"Zhongguancun Laboratory, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-6848-3105","authenticated-orcid":false,"given":"Jingyu","family":"Ke","sequence":"additional","affiliation":[{"name":"Shanghai Jiao Tong University, Shanghai, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0002-9919-6340","authenticated-orcid":false,"given":"Shiyang","family":"Wu","sequence":"additional","affiliation":[{"name":"Shanghai Jiao Tong University, Shanghai, China"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,1,8]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81688-9_1"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1145\/3434333"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-22308-2_3"},{"key":"e_1_3_2_5_2","volume-title":"Principles of model checking","author":"Christel Baier","year":"2008","unstructured":"Christel Baier and Joost-Pieter Katoen. 2008. Principles of model checking. MIT Press."},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-13185-1_3"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2934554"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-31784-3_15"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-45190-5_28"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1145\/3632935"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-30820-8_25"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81688-9_25"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523721"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523721"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509546"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_34"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41528-4_1"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837639"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/3174800"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009873"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_44"},{"key":"e_1_3_2_22_2","first-page":"337","volume-title":"In Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (Budapest, Hungary) (TACAS'08\/ETAPS'08)","author":"Leonardo De Moura","year":"2008","unstructured":"Leonardo De Moura and Nikolaj Bj\u00f8rner. 2008. Z3: An Efficient SMT Solver. In Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (Budapest, Hungary) (TACAS'08\/ETAPS'08). Springer-Verlag, Berlin, Heidelberg, 337-340."},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45069-6_2"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-23702-7_26"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1080\/00029890.1971.11992788"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/3586051"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-68167-2_26"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-11245-5_22"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41528-4_4"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.1145\/2593882.2593900"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40196-1_17"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1145\/3371105"},{"key":"e_1_3_2_33_2","doi-asserted-by":"crossref","unstructured":"William B.Jones and W. J. Thron. 1984. Continued Fractions: Analytic Theory and Applications.https:\/\/api.semanticscholar.org\/CorpusID:118226015","DOI":"10.1017\/CBO9780511759550"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49498-1_15"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1145\/3208102"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","unstructured":"Andrey Kofnov Marcel Moosbrugger Miroslav Stankovic Ezio Bartocci and Efstathia Bura. 2023. Exact and Approximate Moment Derivation for Probabilistic Loops With Non-Polynomial Assignments. CoRR abs\/2306.07072 (2023). https:\/\/doi.org\/10.48550\/ARXIV.2306.07072arXiv:2306.0707210.48550\/ARXIV.2306.07072arXiv:2306.07072","DOI":"10.48550\/ARXIV.2306.07072arXiv:2306.07072"},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(81)90036-2"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25543-5_21"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17465-1_8"},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","DOI":"10.1109\/APSEC57359.2022.00023"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01580665"},{"key":"e_1_3_2_42_2","doi-asserted-by":"publisher","DOI":"10.1145\/3563341"},{"key":"e_1_3_2_43_2","unstructured":"Theodore Samuel Motzkin. 1936. Beitr\u00e4ge zur Theorie der linearen Ungleichungen. (No Title) (1936)."},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","DOI":"10.1145\/3632872"},{"key":"e_1_3_2_45_2","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192394"},{"issue":"3","key":"e_1_3_2_46_2","doi-asserted-by":"crossref","first-page":"969","DOI":"10.1512\/iumj.1993.42.42045","article-title":"Positive Polynomials on Compact Semi-algebraic Sets","volume":"42","author":"Mihai Putinar","year":"1993","unstructured":"Mihai Putinar. 1993. Positive Polynomials on Compact Semi-algebraic Sets. Indiana University Mathematics fournal 42, 3 (1993), 969-984. http:\/\/www.jstor.org\/stable\/24897130","journal-title":"Indiana University Mathematics fournal"},{"key":"e_1_3_2_47_2","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462179"},{"key":"e_1_3_2_48_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27864-1_7"},{"key":"e_1_3_2_49_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-40922-X_8"},{"key":"e_1_3_2_50_2","doi-asserted-by":"publisher","DOI":"10.1145\/3290352"},{"key":"e_1_3_2_51_2","doi-asserted-by":"publisher","DOI":"10.1145\/3450967"},{"key":"e_1_3_2_52_2","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 http:\/\/arxiv.org\/abs\/1809.10756"},{"key":"e_1_3_2_53_2","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454062"},{"key":"e_1_3_2_54_2","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454102"},{"key":"e_1_3_2_55_2","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314581"},{"key":"e_1_3_2_56_2","doi-asserted-by":"publisher","DOI":"10.1145\/3656432"},{"key":"e_1_3_2_57_2","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511813658","volume-title":"Probability with Martingales","author":"David Williams","year":"1991","unstructured":"David Williams. 1991. Probability with Martingales. Cambridge University Press."},{"key":"e_1_3_2_58_2","doi-asserted-by":"publisher","unstructured":"Tengshun Yang Shenghua Feng Hongfei Fu Naijun Zhan Jingyu Ke and Shiyang Wu. 2025. Artifact of POPL 560. (10 2025). https:\/\/doi.org\/10.6084\/m9.figshare.30354097.v4 10.6084\/m9.figshare.30354097.v4","DOI":"10.6084\/m9.figshare.30354097.v4"},{"key":"e_1_3_2_59_2","unstructured":"Tengshun Yang Hongfei Fu Jingyu Ke Naijun Zhan and Shiyang Wu. 2024. Piecewise Linear Expectation Analysis via k-Induction for Probabilistic Programs. CoRR abs\/2403.17567 (2024)."},{"key":"e_1_3_2_60_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\/3776709","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T13:44:37Z","timestamp":1784209477000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3776709"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,1,8]]},"references-count":59,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2026,1,8]]}},"alternative-id":["10.1145\/3776709"],"URL":"https:\/\/doi.org\/10.1145\/3776709","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,1,8]]},"assertion":[{"value":"2025-07-10","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-11-06","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-01-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}