{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,29]],"date-time":"2025-11-29T08:04:36Z","timestamp":1764403476543,"version":"3.46.0"},"publisher-location":"Cham","reference-count":66,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031906527"},{"type":"electronic","value":"9783031906534"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T00:00:00Z","timestamp":1746057600000},"content-version":"vor","delay-in-days":120,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>We consider the problem of refuting equivalence of probabilistic programs, i.e., the problem of proving that two probabilistic programs induce different output distributions. We study this problem in the context of programs with conditioning (i.e., with observe and score statements), where the output distribution is conditioned by the event that all the observe statements along a run evaluate to true, and where the probability densities of different runs may be updated via the score statements. Building on a recent work on programs without conditioning, we present a new equivalence refutation method for programs with conditioning. Our method is based on weighted restarting, a novel transformation of probabilistic programs with conditioning to the output equivalent probabilistic programs without conditioning that we introduce in this work. Our method is the first to be both a)\u00a0fully automated, and b)\u00a0providing provably correct answers. We demonstrate the applicability of our method on a set of programs from the probabilistic inference literature.<\/jats:p>","DOI":"10.1007\/978-3-031-90653-4_14","type":"book-chapter","created":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T08:25:40Z","timestamp":1746174340000},"page":"279-300","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Refuting Equivalence in Probabilistic Programs with Conditioning"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4561-241X","authenticated-orcid":false,"given":"Krishnendu","family":"Chatterjee","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8595-0587","authenticated-orcid":false,"given":"Ehsan","family":"Kafshdar Goharshady","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5026-4392","authenticated-orcid":false,"given":"Petr","family":"Novotn\u00fd","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4681-1699","authenticated-orcid":false,"given":"\u0110or\u0111e","family":"\u017dikeli\u0107","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,5,1]]},"reference":[{"key":"14_CR1","doi-asserted-by":"crossref","unstructured":"Agrawal, S., Chatterjee, K., Novotn\u00fd, P.: Lexicographic ranking supermartingales: an efficient approach to termination of probabilistic programs. Proc. ACM Program. Lang. 2(POPL) (2018)","DOI":"10.1145\/3158122"},{"key":"14_CR2","doi-asserted-by":"publisher","unstructured":"Aguirre, A., Barthe, G., Hsu, J., Kaminski, B.L., Katoen, J., Matheja, C.: A pre-expectation calculus for probabilistic sensitivity. Proc. ACM Program. Lang. 5(POPL), 1\u201328 (2021). https:\/\/doi.org\/10.1145\/3434333","DOI":"10.1145\/3434333"},{"key":"14_CR3","doi-asserted-by":"publisher","unstructured":"Albarghouthi, A., Hsu, J.: Synthesizing coupling proofs of differential privacy. Proc. ACM Program. Lang. 2(POPL), 58:1\u201358:30 (2018). https:\/\/doi.org\/10.1145\/3158146","DOI":"10.1145\/3158146"},{"key":"14_CR4","doi-asserted-by":"publisher","unstructured":"Asadi, A., Chatterjee, K., Fu, H., Goharshady, A.K., Mahdavi, M.: Polynomial reachability witnesses via stellens\u00e4tze. In: Freund, S.N., Yahav, E. (eds.) PLDI \u201921: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Virtual Event, Canada, June 20-25, 2021. pp. 772\u2013787. ACM (2021). https:\/\/doi.org\/10.1145\/3453483.3454076","DOI":"10.1145\/3453483.3454076"},{"key":"14_CR5","doi-asserted-by":"publisher","unstructured":"Avanzini, M., Moser, G., Schaper, M.: A modular cost analysis for probabilistic programs. Proc. ACM Program. Lang. 4(OOPSLA) (nov 2020). https:\/\/doi.org\/10.1145\/3428240","DOI":"10.1145\/3428240"},{"key":"14_CR6","doi-asserted-by":"publisher","unstructured":"Barthe, G., Espitau, T., Gr\u00e9goire, B., Hsu, J., Strub, P.: Proving expected sensitivity of probabilistic programs. Proc. ACM Program. Lang. 2(POPL), 57:1\u201357:29 (2018). https:\/\/doi.org\/10.1145\/3158145","DOI":"10.1145\/3158145"},{"key":"14_CR7","doi-asserted-by":"publisher","unstructured":"Barthe, G., Gaboardi, M., Gr\u00e9goire, B., Hsu, J., Strub, P.: Proving differential privacy via probabilistic couplings. In: Grohe, M., Koskinen, E., Shankar, N. (eds.) Proceedings of the 31st Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS \u201916, New York, NY, USA, July 5-8, 2016. pp. 749\u2013758. ACM (2016). https:\/\/doi.org\/10.1145\/2933575.2934554","DOI":"10.1145\/2933575.2934554"},{"key":"14_CR8","doi-asserted-by":"publisher","unstructured":"Barthe, G., Gaboardi, M., Hsu, J., Pierce, B.C.: Programming language techniques for differential privacy. ACM SIGLOG News 3(1), 34\u201353 (2016). https:\/\/doi.org\/10.1145\/2893582.2893591","DOI":"10.1145\/2893582.2893591"},{"key":"14_CR9","doi-asserted-by":"publisher","unstructured":"Batu, T., Fortnow, L., Rubinfeld, R., Smith, W.D., White, P.: Testing closeness of discrete distributions. J. ACM 60(1), 4:1\u20134:25 (2013). https:\/\/doi.org\/10.1145\/2432622.2432626","DOI":"10.1145\/2432622.2432626"},{"key":"14_CR10","doi-asserted-by":"crossref","unstructured":"Batz, K., Chen, M., Junges, S., Kaminski, B.L., Katoen, J., Matheja, C.: Probabilistic program verification via inductive synthesis of inductive invariants. In: TACAS (2023)","DOI":"10.1007\/978-3-031-30820-8_25"},{"key":"14_CR11","doi-asserted-by":"crossref","unstructured":"Beutner, R., Ong, C.L., Zaiser, F.: Guaranteed bounds for posterior inference in universal probabilistic programming. In: PLDI. pp. 536\u2013551. ACM (2022)","DOI":"10.1145\/3519939.3523721"},{"key":"14_CR12","doi-asserted-by":"publisher","unstructured":"Bichsel, B., Gehr, T., Vechev, M.T.: Fine-grained semantics for probabilistic programs. In: Ahmed, A. (ed.) Programming Languages and Systems - 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings. Lecture Notes in Computer Science, vol. 10801, pp. 145\u2013185. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-89884-1_6, https:\/\/doi.org\/10.1007\/978-3-319-89884-1_6","DOI":"10.1007\/978-3-319-89884-1_6"},{"key":"14_CR13","doi-asserted-by":"crossref","unstructured":"Canonne, C.L.: A survey on distribution testing: Your data is big. but is it blue? Theory of Computing pp. 1\u2013100 (2020)","DOI":"10.4086\/toc.gs.2020.009"},{"key":"14_CR14","doi-asserted-by":"crossref","unstructured":"Chakarov, A., Sankaranarayanan, S.: Probabilistic program analysis with martingales. In: CAV (2013)","DOI":"10.1007\/978-3-642-39799-8_34"},{"key":"14_CR15","doi-asserted-by":"publisher","unstructured":"Chakraborty, S., Meel, K.S.: On testing of uniform samplers. In: The Thirty-Third AAAI Conference on Artificial Intelligence, AAAI 2019, The Thirty-First Innovative Applications of Artificial Intelligence Conference, IAAI 2019, The Ninth AAAI Symposium on Educational Advances in Artificial Intelligence, EAAI 2019, Honolulu, Hawaii, USA, January 27 - February 1, 2019. pp. 7777\u20137784. AAAI Press (2019). https:\/\/doi.org\/10.1609\/aaai.v33i01.33017777","DOI":"10.1609\/aaai.v33i01.33017777"},{"key":"14_CR16","doi-asserted-by":"publisher","unstructured":"Chan, S., Diakonikolas, I., Valiant, P., Valiant, G.: Optimal algorithms for testing closeness of discrete distributions. In: Chekuri, C. (ed.) Proceedings of the Twenty-Fifth Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2014, Portland, Oregon, USA, January 5-7, 2014. pp. 1193\u20131203. SIAM (2014). https:\/\/doi.org\/10.1137\/1.9781611973402.88","DOI":"10.1137\/1.9781611973402.88"},{"key":"14_CR17","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Fu, H., Goharshady, A.K.: Termination analysis of probabilistic programs through positivstellensatz\u2019s. In: CAV (2016)","DOI":"10.1007\/978-3-319-41528-4_1"},{"key":"14_CR18","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Fu, H., Goharshady, A.K., Goharshady, E.K.: Polynomial invariant generation for non-deterministic recursive programs. In: PLDI. pp. 672\u2013687. ACM (2020)","DOI":"10.1145\/3385412.3385969"},{"key":"14_CR19","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Fu, H., Novotn\u00fd, P., Hasheminezhad, R.: Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs. ACM Trans. Program. Lang. Syst. 40(2) (2018)","DOI":"10.1145\/3174800"},{"key":"14_CR20","doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Goharshady, A.K., Meggendorfer, T., Zikelic, D.: Sound and complete certificates for quantitative termination analysis of probabilistic programs. In: Shoham, S., Vizel, Y. (eds.) Computer Aided Verification - 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part I. Lecture Notes in Computer Science, vol. 13371, pp. 55\u201378. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-13185-1_4","DOI":"10.1007\/978-3-031-13185-1_4"},{"key":"14_CR21","doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Goharshady, A.K., Meggendorfer, T., Zikelic, D.: Quantitative bounds on resource usage of probabilistic programs. Proc. ACM Program. Lang. 8(OOPSLA1), 362\u2013391 (2024). https:\/\/doi.org\/10.1145\/3649824, https:\/\/doi.org\/10.1145\/3649824","DOI":"10.1145\/3649824"},{"key":"14_CR22","doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Goharshady, E.K., Novotn\u00fd, P., Z\u00e1rev\u00facky, J., Zikelic, D.: On lexicographic proof rules for probabilistic termination. In: Huisman, M., Pasareanu, C.S., Zhan, N. (eds.) Formal Methods - 24th International Symposium, FM 2021, Virtual Event, November 20-26, 2021, Proceedings. Lecture Notes in Computer Science, vol. 13047, pp. 619\u2013639. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-90870-6_33","DOI":"10.1007\/978-3-030-90870-6_33"},{"key":"14_CR23","doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Goharshady, E.K., Novotn\u00fd, P., Zikelic, D.: Equivalence and similarity refutation for probabilistic programs. Proc. ACM Program. Lang. 8(PLDI), 2098\u20132122 (2024). https:\/\/doi.org\/10.1145\/3656462, https:\/\/doi.org\/10.1145\/3656462","DOI":"10.1145\/3656462"},{"key":"14_CR24","unstructured":"Chatterjee, K., Goharshady, E.K., Novotn\u00fd, P., \u0110or\u0111e \u017dikeli\u0107: Refuting equivalence in probabilistic programs with conditioning (2025), https:\/\/arxiv.org\/abs\/2501.06579"},{"key":"14_CR25","doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Novotn\u00fd, P., Zikelic, D.: Stochastic invariants for probabilistic termination. In: Castagna, G., Gordon, A.D. (eds.) Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017. pp. 145\u2013160. ACM (2017). https:\/\/doi.org\/10.1145\/3009837.3009873","DOI":"10.1145\/3009837.3009873"},{"key":"14_CR26","doi-asserted-by":"publisher","unstructured":"Chen, J., He, F.: Proving almost-sure termination by omega-regular decomposition. In: Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI\u201920). p. 869-882. PLDI 2020, Association for Computing Machinery, New York, NY, USA (2020). https:\/\/doi.org\/10.1145\/3385412.3386002","DOI":"10.1145\/3385412.3386002"},{"key":"14_CR27","doi-asserted-by":"publisher","unstructured":"Chen, M., Katoen, J., Klinkenberg, L., Winkler, T.: Does a program yield the right distribution? - verifying probabilistic programs via generating functions. In: Shoham, S., Vizel, Y. (eds.) Computer Aided Verification - 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part I. Lecture Notes in Computer Science, vol. 13371, pp. 79\u2013101. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-13185-1_5","DOI":"10.1007\/978-3-031-13185-1_5"},{"key":"14_CR28","unstructured":"Cusumano-Towner, M.F., Mansinghka, V.K.: AIDE: an algorithm for measuring the accuracy of probabilistic inference algorithms. In: NIPS. pp. 3000\u20133010 (2017)"},{"key":"14_CR29","doi-asserted-by":"publisher","unstructured":"Das, A., Wang, D., Hoffmann, J.: Probabilistic resource-aware session types. Proc. ACM Program. Lang. 7(POPL) (jan 2023). https:\/\/doi.org\/10.1145\/3571259","DOI":"10.1145\/3571259"},{"key":"14_CR30","unstructured":"Domke, J.: An easy to interpret diagnostic for approximate inference: Symmetric divergence over simulations. CoRR abs\/2103.01030 (2021)"},{"key":"14_CR31","doi-asserted-by":"crossref","unstructured":"Feautrier, P., Gonnord, L.: Accelerated invariant generation for C programs with aspic and c2fsm. In: TAPAS@SAS (2010)","DOI":"10.1016\/j.entcs.2010.09.014"},{"key":"14_CR32","doi-asserted-by":"publisher","unstructured":"Fioriti, L.M.F., Hermanns, H.: Probabilistic Termination: Soundness, Completeness, and Compositionality. In: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2015). pp. 489\u2013501 (2015). https:\/\/doi.org\/10.1145\/2676726.2677001","DOI":"10.1145\/2676726.2677001"},{"key":"14_CR33","doi-asserted-by":"publisher","unstructured":"Foster, N., Kozen, D., Mamouras, K., Reitblatt, M., Silva, A.: Probabilistic netkat. In: Thiemann, P. (ed.) Programming Languages and Systems - 25th European Symposium on Programming, ESOP 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings. Lecture Notes in Computer Science, vol.\u00a09632, pp. 282\u2013309. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-662-49498-1_12","DOI":"10.1007\/978-3-662-49498-1_12"},{"key":"14_CR34","doi-asserted-by":"crossref","unstructured":"Gehr, T., Misailovic, S., Vechev, M.T.: PSI: exact symbolic inference for probabilistic programs. In: CAV (2016)","DOI":"10.1007\/978-3-319-41528-4_4"},{"key":"14_CR35","doi-asserted-by":"publisher","unstructured":"Ghahramani, Z.: Probabilistic machine learning and artificial intelligence. Nat. 521(7553), 452\u2013459 (2015). https:\/\/doi.org\/10.1038\/nature14541","DOI":"10.1038\/nature14541"},{"key":"14_CR36","doi-asserted-by":"publisher","unstructured":"Goldblatt, R., Jackson, M.: Well-structured program equivalence is highly undecidable. ACM Trans. Comput. Log. 13(3), 26:1\u201326:8 (2012). https:\/\/doi.org\/10.1145\/2287718.2287726, https:\/\/doi.org\/10.1145\/2287718.2287726","DOI":"10.1145\/2287718.2287726"},{"key":"14_CR37","doi-asserted-by":"publisher","unstructured":"Gregersen, S.O., Aguirre, A., Haselwarter, P.G., Tassarotti, J., Birkedal, L.: Asynchronous probabilistic couplings in higher-order separation logic. Proc. ACM Program. Lang. 8(POPL), 753\u2013784 (2024). https:\/\/doi.org\/10.1145\/3632868","DOI":"10.1145\/3632868"},{"key":"14_CR38","unstructured":"Grosse, R.B., Ancha, S., Roy, D.M.: Measuring the reliability of MCMC inference with bidirectional monte carlo. In: NIPS. pp. 2451\u20132459 (2016)"},{"key":"14_CR39","unstructured":"Grosse, R.B., Ghahramani, Z., Adams, R.P.: Sandwiching the marginal likelihood using bidirectional monte carlo. CoRR abs\/1511.02543 (2015)"},{"key":"14_CR40","unstructured":"Gurobi Optimization, LLC: Gurobi Optimizer Reference Manual (2023), https:\/\/www.gurobi.com"},{"key":"14_CR41","doi-asserted-by":"crossref","unstructured":"Handelman, D.: Representing polynomials by positive linear functions on compact convex polyhedra. Pacific Journal of Mathematics 132(1) (1988)","DOI":"10.2140\/pjm.1988.132.35"},{"key":"14_CR42","doi-asserted-by":"publisher","unstructured":"Huang, Z., Wang, Z., Misailovic, S.: Psense: Automatic sensitivity analysis for probabilistic programs. In: Lahiri, S.K., Wang, C. (eds.) Automated Technology for Verification and Analysis - 16th International Symposium, ATVA 2018, Los Angeles, CA, USA, October 7-10, 2018, Proceedings. Lecture Notes in Computer Science, vol. 11138, pp. 387\u2013403. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-030-01090-4_23","DOI":"10.1007\/978-3-030-01090-4_23"},{"key":"14_CR43","doi-asserted-by":"publisher","unstructured":"Katoen, J.P., Gretz, F., Jansen, N., Kaminski, B.L., Olmedo, F.: Understanding Probabilistic Programs, pp. 15\u201332. Springer International Publishing, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-23506-6_4","DOI":"10.1007\/978-3-319-23506-6_4"},{"key":"14_CR44","doi-asserted-by":"crossref","unstructured":"Kura, S., Urabe, N., Hasuo, I.: Tail probabilities for randomized program runtimes via martingales for higher moments. In: TACAS (2). Lecture Notes in Computer Science, vol. 11428, pp. 135\u2013153. Springer (2019)","DOI":"10.1007\/978-3-030-17465-1_8"},{"key":"14_CR45","doi-asserted-by":"crossref","unstructured":"Legay, A., Murawski, A.S., Ouaknine, J., Worrell, J.: On automated verification of probabilistic programs. In: TACAS. Lecture Notes in Computer Science, vol.\u00a04963, pp. 173\u2013187. Springer (2008)","DOI":"10.1007\/978-3-540-78800-3_13"},{"key":"14_CR46","doi-asserted-by":"publisher","unstructured":"Majumdar, R., Sathiyanarayana, V.R.: Positive almost-sure termination: Complexity and proof rules. Proc. ACM Program. Lang. 8(POPL) (jan 2024). https:\/\/doi.org\/10.1145\/3632879","DOI":"10.1145\/3632879"},{"key":"14_CR47","doi-asserted-by":"crossref","unstructured":"McIver, A., Morgan, C.: Abstraction, Refinement and Proof for Probabilistic Systems. Monographs in Computer Science, Springer (2005)","DOI":"10.1145\/1059816.1059824"},{"key":"14_CR48","doi-asserted-by":"crossref","unstructured":"McIver, A., Morgan, C.: Correctness by construction for probabilistic programs. In: ISoLA (1). Lecture Notes in Computer Science, vol. 12476, pp. 216\u2013239. Springer (2020)","DOI":"10.1007\/978-3-030-61362-4_12"},{"key":"14_CR49","doi-asserted-by":"publisher","unstructured":"McIver, A., Morgan, C., Kaminski, B.L., Katoen, J.: A new proof rule for almost-sure termination. Proc. ACM Program. Lang. 2(POPL), 33:1\u201333:28 (2018). https:\/\/doi.org\/10.1145\/3158121","DOI":"10.1145\/3158121"},{"key":"14_CR50","unstructured":"Meyn, S.P., Tweedie, R.L.: Markov chains and stochastic stability. Springer Science & Business Media (2012)"},{"key":"14_CR51","doi-asserted-by":"publisher","unstructured":"Murawski, A.S., Ouaknine, J.: On probabilistic program equivalence and refinement. In: Abadi, M., de\u00a0Alfaro, L. (eds.) CONCUR 2005 - Concurrency Theory, 16th International Conference, CONCUR 2005, San Francisco, CA, USA, August 23-26, 2005, Proceedings. Lecture Notes in Computer Science, vol.\u00a03653, pp. 156\u2013170. Springer (2005). https:\/\/doi.org\/10.1007\/11539452_15, https:\/\/doi.org\/10.1007\/11539452_15","DOI":"10.1007\/11539452_15"},{"key":"14_CR52","doi-asserted-by":"publisher","unstructured":"Ngo, V.C., Carbonneaux, Q., Hoffmann, J.: Bounded expectations: resource analysis for probabilistic programs. In: Foster, J.S., Grossman, D. (eds.) Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018, Philadelphia, PA, USA, June 18-22, 2018. pp. 496\u2013512. ACM (2018). https:\/\/doi.org\/10.1145\/3192366.3192394","DOI":"10.1145\/3192366.3192394"},{"key":"14_CR53","doi-asserted-by":"publisher","unstructured":"Olmedo, F., Gretz, F., Jansen, N., Kaminski, B.L., Katoen, J., McIver, A.: Conditioning in probabilistic programming. ACM Trans. Program. Lang. Syst. 40(1), 4:1\u20134:50 (2018). https:\/\/doi.org\/10.1145\/3156018","DOI":"10.1145\/3156018"},{"key":"14_CR54","doi-asserted-by":"publisher","unstructured":"Sankaranarayanan, S., Chakarov, A., Gulwani, S.: Static analysis for probabilistic programs: inferring whole program properties from finitely many paths. In: Boehm, H., Flanagan, C. (eds.) ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI \u201913, Seattle, WA, USA, June 16-19, 2013. pp. 447\u2013458. ACM (2013). https:\/\/doi.org\/10.1145\/2491956.2462179","DOI":"10.1145\/2491956.2462179"},{"key":"14_CR55","doi-asserted-by":"crossref","unstructured":"Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Constraint-based linear-relations analysis. In: SAS (2004)","DOI":"10.1007\/978-3-540-27864-1_7"},{"key":"14_CR56","doi-asserted-by":"publisher","unstructured":"Takisaka, T., Oyabu, Y., Urabe, N., Hasuo, I.: Ranking and repulsing supermartingales for reachability in randomized programs. ACM Trans. Program. Lang. Syst. 43(2), 5:1\u20135:46 (2021). https:\/\/doi.org\/10.1145\/3450967","DOI":"10.1145\/3450967"},{"key":"14_CR57","doi-asserted-by":"publisher","unstructured":"Takisaka, T., Zhang, L., Wang, C., Liu, J.: Fairness in ranking supermartingales. CoRR abs\/2304.11363 (2023). https:\/\/doi.org\/10.48550\/ARXIV.2304.11363","DOI":"10.48550\/ARXIV.2304.11363"},{"key":"14_CR58","doi-asserted-by":"publisher","unstructured":"Thrun, S.: Probabilistic algorithms in robotics. AI Mag. 21(4), 93\u2013109 (2000). https:\/\/doi.org\/10.1609\/aimag.v21i4.1534","DOI":"10.1609\/aimag.v21i4.1534"},{"key":"14_CR59","unstructured":"Villani, C.: Topics in optimal transportation, vol.\u00a058. American Mathematical Soc. (2021)"},{"key":"14_CR60","doi-asserted-by":"publisher","unstructured":"Wang, D., Hoffmann, J., Reps, T.W.: Central moment analysis for cost accumulators in probabilistic programs. In: Freund, S.N., Yahav, E. (eds.) PLDI \u201921: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Virtual Event, Canada, June 20-25, 2021. pp. 559\u2013573. ACM (2021). https:\/\/doi.org\/10.1145\/3453483.3454062","DOI":"10.1145\/3453483.3454062"},{"key":"14_CR61","doi-asserted-by":"publisher","unstructured":"Wang, P., Fu, H., Chatterjee, K., Deng, Y., Xu, M.: Proving expected sensitivity of probabilistic programs with randomized variable-dependent termination time. Proc. ACM Program. Lang. 4(POPL), 25:1\u201325:30 (2020). https:\/\/doi.org\/10.1145\/3371093","DOI":"10.1145\/3371093"},{"key":"14_CR62","doi-asserted-by":"crossref","unstructured":"Wang, P., Fu, H., Goharshady, A.K., Chatterjee, K., Qin, X., Shi, W.: Cost analysis of nondeterministic probabilistic programs. In: PLDI (2019)","DOI":"10.1145\/3314221.3314581"},{"key":"14_CR63","doi-asserted-by":"publisher","unstructured":"Wang, P., Yang, T., Fu, H., Li, G., Ong, C.L.: Static posterior inference of bayesian probabilistic programming via polynomial solving. Proc. ACM Program. Lang. 8(PLDI), 1361\u20131386 (2024). https:\/\/doi.org\/10.1145\/3656432, https:\/\/doi.org\/10.1145\/3656432","DOI":"10.1145\/3656432"},{"key":"14_CR64","unstructured":"Williams, D.: Probability with Martingales. Cambridge mathematical textbooks, Cambridge University Press (1991)"},{"key":"14_CR65","unstructured":"Wolfram Research, Inc.: Mathematica 13.2 (2022), https:\/\/www.wolfram.com"},{"key":"14_CR66","doi-asserted-by":"publisher","unstructured":"Zikelic, D., Chang, B.E., Bolignano, P., Raimondi, F.: Differential cost analysis with simultaneous potentials and anti-potentials. In: Jhala, R., Dillig, I. (eds.) PLDI \u201922: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, San Diego, CA, USA, June 13 - 17, 2022. pp. 442\u2013457. ACM (2022). https:\/\/doi.org\/10.1145\/3519939.3523435","DOI":"10.1145\/3519939.3523435"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-90653-4_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,29]],"date-time":"2025-11-29T07:36:52Z","timestamp":1764401812000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-90653-4_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031906527","9783031906534"],"references-count":66,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-90653-4_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"1 May 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Hamilton, ON","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 May 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 May 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2025\/conferences\/tacas\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}