{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,11]],"date-time":"2026-05-11T11:20:37Z","timestamp":1778498437365,"version":"3.51.4"},"publisher-location":"Cham","reference-count":60,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031757822","type":"print"},{"value":"9783031757839","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,11,13]],"date-time":"2024-11-13T00:00:00Z","timestamp":1731456000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,11,13]],"date-time":"2024-11-13T00:00:00Z","timestamp":1731456000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"DOI":"10.1007\/978-3-031-75783-9_10","type":"book-chapter","created":{"date-parts":[[2024,11,12]],"date-time":"2024-11-12T06:27:04Z","timestamp":1731392824000},"page":"230-254","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["A Unified Framework for\u00a0Quantitative Analysis of\u00a0Probabilistic Programs"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5352-4954","authenticated-orcid":false,"given":"Shenghua","family":"Feng","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2072-0836","authenticated-orcid":false,"given":"Tengshun","family":"Yang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9663-7441","authenticated-orcid":false,"given":"Mingshuai","family":"Chen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3298-3817","authenticated-orcid":false,"given":"Naijun","family":"Zhan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,11,13]]},"reference":[{"key":"10_CR1","doi-asserted-by":"crossref","unstructured":"A.\u00a0Abate, M.\u00a0Giacobbe, and D.\u00a0Roy. Learning probabilistic termination proofs. In A.\u00a0Silva and K.\u00a0R.\u00a0M. Leino, editors, Computer Aided Verification - 33rd International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part II, volume 12760 of Lecture Notes in Computer Science, pages 3\u201326. Springer, 2021","DOI":"10.1007\/978-3-030-81688-9_1"},{"key":"10_CR2","doi-asserted-by":"crossref","unstructured":"A.\u00a0Albarghouthi and J.\u00a0Hsu. Constraint-based synthesis of coupling proofs. In H.\u00a0Chockler and G.\u00a0Weissenbacher, editors, Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part I, volume 10981 of Lecture Notes in Computer Science, pages 327\u2013346. Springer, 2018","DOI":"10.1007\/978-3-319-96145-3_18"},{"key":"10_CR3","doi-asserted-by":"crossref","unstructured":"A.\u00a0Albarghouthi and J.\u00a0Hsu. Synthesizing coupling proofs of differential privacy. Proc. ACM Program. Lang., 2(POPL):58:1\u201358:30, 2018","DOI":"10.1145\/3158146"},{"issue":"4","key":"10_CR4","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1016\/0020-0190(85)90056-0","volume":"21","author":"B Alpern","year":"1985","unstructured":"Alpern, B., Schneider, F.B.: Defining liveness. Inf. Process. Lett. 21(4), 181\u2013185 (1985)","journal-title":"Inf. Process. Lett."},{"key":"10_CR5","doi-asserted-by":"crossref","unstructured":"D.\u00a0Amrollahi, E.\u00a0Bartocci, G.\u00a0Kenison, L.\u00a0Kov\u00e1cs, M.\u00a0Moosbrugger, and M.\u00a0Stankovic. Solving invariant generation for unsolvable loops. In G.\u00a0Singh and C.\u00a0Urban, editors, Static Analysis - 29th International Symposium, SAS 2022, Auckland, New Zealand, December 5-7, 2022, Proceedings, volume 13790 of Lecture Notes in Computer Science, pages 19\u201343. Springer, 2022","DOI":"10.1007\/978-3-031-22308-2_3"},{"issue":"2","key":"10_CR6","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/s10107-002-0349-3","volume":"95","author":"ED Andersen","year":"2003","unstructured":"Andersen, E.D., Roos, C., Terlaky, T.: On implementing a primal-dual interior-point method for conic quadratic optimization. Math. Program. 95(2), 249\u2013277 (2003)","journal-title":"Math. Program."},{"key":"10_CR7","unstructured":"C.\u00a0Baier and J.\u00a0Katoen. Principles of model checking. MIT Press, 2008"},{"key":"10_CR8","doi-asserted-by":"crossref","unstructured":"C.\u00a0Baier, J.\u00a0Klein, L.\u00a0Leuschner, D.\u00a0Parker, and S.\u00a0Wunderlich. Ensuring the reliability of your model checker: Interval iteration for markov decision processes. In R.\u00a0Majumdar and V.\u00a0Kuncak, editors, Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I, volume 10426 of Lecture Notes in Computer Science, pages 160\u2013180. Springer, 2017","DOI":"10.1007\/978-3-319-63387-9_8"},{"key":"10_CR9","doi-asserted-by":"crossref","unstructured":"G.\u00a0Barthe, M.\u00a0Gaboardi, B.\u00a0Gr\u00e9goire, J.\u00a0Hsu, and P.\u00a0Strub. Proving differential privacy via probabilistic couplings. In M.\u00a0Grohe, E.\u00a0Koskinen, and N.\u00a0Shankar, editors, Proceedings of the 31st Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS \u201916, New York, NY, USA, July 5-8, 2016, pages 749\u2013758. ACM, 2016","DOI":"10.1145\/2933575.2934554"},{"key":"10_CR10","doi-asserted-by":"crossref","unstructured":"G.\u00a0Barthe, J.-P. Katoen, and E.\u00a0A.\u00a0Silva. Foundations of Probabilistic Programming. Cambridge University Press, 2020","DOI":"10.1017\/9781108770750"},{"key":"10_CR11","doi-asserted-by":"crossref","unstructured":"K.\u00a0Batz, M.\u00a0Chen, S.\u00a0Junges, B.\u00a0L. Kaminski, J.\u00a0Katoen, and C.\u00a0Matheja. Probabilistic program verification via inductive synthesis of inductive invariants. In S.\u00a0Sankaranarayanan and N.\u00a0Sharygina, editors, Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Paris, France, April 22-27, 2023, Proceedings, Part II, volume 13994 of Lecture Notes in Computer Science, pages 410\u2013429. Springer, 2023","DOI":"10.1007\/978-3-031-30820-8_25"},{"issue":"OOPSLA1","key":"10_CR12","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3527310","volume":"6","author":"K Batz","year":"2022","unstructured":"Batz, K., Gallus, A., Kaminski, B.L., Katoen, J., Winkler, T.: Weighted programming: a programming paradigm for specifying mathematical models. Proc. ACM Program. Lang. 6(OOPSLA1), 1\u201330 (2022)","journal-title":"Proc. ACM Program. Lang."},{"key":"10_CR13","doi-asserted-by":"crossref","unstructured":"R.\u00a0Beutner, C.\u00a0L. Ong, and F.\u00a0Zaiser. Guaranteed bounds for posterior inference in universal probabilistic programming. In R.\u00a0Jhala and I.\u00a0Dillig, editors, PLDI \u201922: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, San Diego, CA, USA, June 13 - 17, 2022, pages 536\u2013551. ACM, 2022","DOI":"10.1145\/3519939.3523721"},{"key":"10_CR14","doi-asserted-by":"crossref","unstructured":"J.\u00a0Borgstr\u00f6m, U.\u00a0D. Lago, A.\u00a0D. Gordon, and M.\u00a0Szymczak. A lambda-calculus foundation for universal probabilistic programming. In J.\u00a0Garrigue, G.\u00a0Keller, and E.\u00a0Sumii, editors, Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Nara, Japan, September 18-22, 2016, pages 33\u201346. ACM, 2016","DOI":"10.1145\/2951913.2951942"},{"key":"10_CR15","doi-asserted-by":"crossref","unstructured":"M.\u00a0Carbin, S.\u00a0Misailovic, and M.\u00a0C. Rinard. Verifying quantitative reliability for programs that execute on unreliable hardware. In A.\u00a0L. Hosking, P.\u00a0T. Eugster, and C.\u00a0V. Lopes, editors, Proceedings of the 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages & Applications, OOPSLA 2013, part of SPLASH 2013, Indianapolis, IN, USA, October 26-31, 2013, pages 33\u201352. ACM, 2013","DOI":"10.1145\/2509136.2509546"},{"key":"10_CR16","unstructured":"A.\u00a0Chakarov and S.\u00a0Sankaranarayanan. Probabilistic program analysis with martingales. In N.\u00a0Sharygina and H.\u00a0Veith, editors, Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings, volume 8044 of Lecture Notes in Computer Science, pages 511\u2013526. Springer, 2013"},{"key":"10_CR17","doi-asserted-by":"crossref","unstructured":"A.\u00a0Chakarov, Y.\u00a0Voronin, and S.\u00a0Sankaranarayanan. Deductive proofs of almost sure persistence and recurrence properties. In M.\u00a0Chechik and J.\u00a0Raskin, editors, Tools and Algorithms for the Construction and Analysis of Systems - 22nd International Conference, TACAS 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, volume 9636 of Lecture Notes in Computer Science, pages 260\u2013279. Springer, 2016","DOI":"10.1007\/978-3-662-49674-9_15"},{"key":"10_CR18","doi-asserted-by":"crossref","unstructured":"K.\u00a0Chatterjee, H.\u00a0Fu, and A.\u00a0K. Goharshady. Termination analysis of probabilistic programs through positivstellensatz\u2019s. In S.\u00a0Chaudhuri and A.\u00a0Farzan, editors, Computer Aided Verification - 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part I, volume 9779 of Lecture Notes in Computer Science, pages 3\u201322. Springer, 2016","DOI":"10.1007\/978-3-319-41528-4_1"},{"key":"10_CR19","doi-asserted-by":"crossref","unstructured":"K.\u00a0Chatterjee, H.\u00a0Fu, and A.\u00a0K. Goharshady. Termination analysis of probabilistic programs through positivstellensatz\u2019s. CoRR, abs\/1604.07169, 2016","DOI":"10.1007\/978-3-319-41528-4_1"},{"key":"10_CR20","doi-asserted-by":"crossref","unstructured":"K.\u00a0Chatterjee, H.\u00a0Fu, P.\u00a0Novotn\u00fd, and R.\u00a0Hasheminezhad. Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs. In R.\u00a0Bod\u00edk and R.\u00a0Majumdar, editors, Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016, pages 327\u2013342. ACM, 2016","DOI":"10.1145\/2837614.2837639"},{"key":"10_CR21","doi-asserted-by":"crossref","unstructured":"K.\u00a0Chatterjee, H.\u00a0Fu, P.\u00a0Novotn\u00fd, and R.\u00a0Hasheminezhad. Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs. ACM Trans. Program. Lang. Syst., 40(2):7:1\u20137:45, 2018","DOI":"10.1145\/3174800"},{"key":"10_CR22","doi-asserted-by":"crossref","unstructured":"K.\u00a0Chatterjee, P.\u00a0Novotn\u00fd, and D.\u00a0Zikelic. Stochastic invariants for probabilistic termination. In G.\u00a0Castagna and A.\u00a0D. Gordon, editors, Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, pages 145\u2013160. ACM, 2017","DOI":"10.1145\/3009837.3009873"},{"key":"10_CR23","doi-asserted-by":"crossref","unstructured":"M.\u00a0Chen, J.\u00a0Katoen, L.\u00a0Klinkenberg, and T.\u00a0Winkler. Does a program yield the right distribution? - verifying probabilistic programs via generating functions. In S.\u00a0Shoham and Y.\u00a0Vizel, editors, Computer Aided Verification - 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part I, volume 13371 of Lecture Notes in Computer Science, pages 79\u2013101. Springer, 2022","DOI":"10.1007\/978-3-031-13185-1_5"},{"key":"10_CR24","unstructured":"E.\u00a0W. Dijkstra. A Discipline of Programming. Prentice-Hall, 1976"},{"key":"10_CR25","doi-asserted-by":"crossref","unstructured":"R.\u00a0Durrett. Probability: theory and examples, volume\u00a049. Cambridge University Press, 2019","DOI":"10.1017\/9781108591034"},{"issue":"OOPSLA1","key":"10_CR26","doi-asserted-by":"publisher","first-page":"696","DOI":"10.1145\/3586051","volume":"7","author":"S Feng","year":"2023","unstructured":"Feng, S., Chen, M., Su, H., Kaminski, B.L., Katoen, J., Zhan, N.: Lower bounds for possibly divergent probabilistic programs. Proc. ACM Program. Lang. 7(OOPSLA1), 696\u2013726 (2023)","journal-title":"Proc. ACM Program. Lang."},{"key":"10_CR27","doi-asserted-by":"crossref","unstructured":"N.\u00a0Foster, D.\u00a0Kozen, K.\u00a0Mamouras, M.\u00a0Reitblatt, and A.\u00a0Silva. Probabilistic netkat. In P.\u00a0Thiemann, editor, 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, volume 9632 of Lecture Notes in Computer Science, pages 282\u2013309. Springer, 2016","DOI":"10.1007\/978-3-662-49498-1_12"},{"key":"10_CR28","doi-asserted-by":"crossref","unstructured":"H.\u00a0Fu and K.\u00a0Chatterjee. Termination of nondeterministic probabilistic programs. In C.\u00a0Enea and R.\u00a0Piskac, editors, Verification, Model Checking, and Abstract Interpretation - 20th International Conference, VMCAI 2019, Cascais, Portugal, January 13-15, 2019, Proceedings, volume 11388 of Lecture Notes in Computer Science, pages 468\u2013490. Springer, 2019","DOI":"10.1007\/978-3-030-11245-5_22"},{"key":"10_CR29","doi-asserted-by":"crossref","unstructured":"A.\u00a0D. Gordon, T.\u00a0A. Henzinger, A.\u00a0V. Nori, and S.\u00a0K. Rajamani. Probabilistic programming. In J.\u00a0D. Herbsleb and M.\u00a0B. Dwyer, editors, Proceedings of the on Future of Software Engineering, FOSE 2014, Hyderabad, India, May 31 - June 7, 2014, pages 167\u2013181. ACM, 2014","DOI":"10.1145\/2593882.2593900"},{"key":"10_CR30","doi-asserted-by":"crossref","unstructured":"M.\u00a0Hark, B.\u00a0L. Kaminski, J.\u00a0Giesl, and J.\u00a0Katoen. Aiming low is harder: induction for lower bounds in probabilistic program verification. Proc. ACM Program. Lang., 4(POPL):37:1\u201337:28, 2020","DOI":"10.1145\/3371105"},{"key":"10_CR31","doi-asserted-by":"crossref","unstructured":"A.\u00a0Hartmanns and B.\u00a0L. Kaminski. Optimistic value iteration. In S.\u00a0K. Lahiri and C.\u00a0Wang, editors, Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part II, volume 12225 of Lecture Notes in Computer Science, pages 488\u2013511. Springer, 2020","DOI":"10.1007\/978-3-030-53291-8_26"},{"key":"10_CR32","unstructured":"B.\u00a0L. Kaminski. Advanced weakest precondition calculi for probabilistic programs. PhD thesis, RWTH Aachen University, Germany, 2019"},{"key":"10_CR33","doi-asserted-by":"crossref","unstructured":"B.\u00a0L. Kaminski and J.\u00a0Katoen. A weakest pre-expectation semantics for mixed-sign expectations. In 32nd Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017, pages 1\u201312. IEEE Computer Society, 2017","DOI":"10.1109\/LICS.2017.8005153"},{"key":"10_CR34","doi-asserted-by":"crossref","unstructured":"B.\u00a0L. Kaminski, J.\u00a0Katoen, C.\u00a0Matheja, and F.\u00a0Olmedo. Weakest precondition reasoning for expected run-times of probabilistic programs. In P.\u00a0Thiemann, editor, 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, volume 9632 of Lecture Notes in Computer Science, pages 364\u2013389. Springer, 2016","DOI":"10.1007\/978-3-662-49498-1_15"},{"key":"10_CR35","doi-asserted-by":"crossref","unstructured":"B.\u00a0L. Kaminski, J.\u00a0Katoen, C.\u00a0Matheja, and F.\u00a0Olmedo. Weakest precondition reasoning for expected runtimes of randomized algorithms. J. ACM, 65(5):30:1\u201330:68, 2018","DOI":"10.1145\/3208102"},{"key":"10_CR36","doi-asserted-by":"crossref","unstructured":"A.\u00a0Karimi, M.\u00a0Moosbrugger, M.\u00a0Stankovic, L.\u00a0Kov\u00e1cs, E.\u00a0Bartocci, and E.\u00a0Bura. Distribution estimation for probabilistic loops. In E.\u00a0\u00c1brah\u00e1m and M.\u00a0Paolieri, editors, Quantitative Evaluation of Systems - 19th International Conference, QEST 2022, Warsaw, Poland, September 12-16, 2022, Proceedings, volume 13479 of Lecture Notes in Computer Science, pages 26\u201342. Springer, 2022","DOI":"10.1007\/978-3-031-16336-4_2"},{"key":"10_CR37","doi-asserted-by":"crossref","unstructured":"L.\u00a0Klinkenberg, K.\u00a0Batz, B.\u00a0L. Kaminski, J.\u00a0Katoen, J.\u00a0Moerman, and T.\u00a0Winkler. Generating functions for probabilistic programs. In M.\u00a0Fern\u00e1ndez, editor, Logic-Based Program Synthesis and Transformation - 30th International Symposium, LOPSTR 2020, Bologna, Italy, September 7-9, 2020, Proceedings, volume 12561 of Lecture Notes in Computer Science, pages 231\u2013248. Springer, 2020","DOI":"10.1007\/978-3-030-68446-4_12"},{"key":"10_CR38","doi-asserted-by":"crossref","unstructured":"A.\u00a0Kofnov, M.\u00a0Moosbrugger, M.\u00a0Stankovic, E.\u00a0Bartocci, and E.\u00a0Bura. Moment-based invariants for probabilistic loops with non-polynomial assignments. In E.\u00a0\u00c1brah\u00e1m and M.\u00a0Paolieri, editors, Quantitative Evaluation of Systems - 19th International Conference, QEST 2022, Warsaw, Poland, September 12-16, 2022, Proceedings, volume 13479 of Lecture Notes in Computer Science, pages 3\u201325. Springer, 2022","DOI":"10.1007\/978-3-031-16336-4_1"},{"issue":"3","key":"10_CR39","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1016\/0022-0000(81)90036-2","volume":"22","author":"D Kozen","year":"1981","unstructured":"Kozen, D.: Semantics of probabilistic programs. J. Comput. Syst. Sci. 22(3), 328\u2013350 (1981)","journal-title":"J. Comput. Syst. Sci."},{"key":"10_CR40","doi-asserted-by":"crossref","unstructured":"S.\u00a0Kura, N.\u00a0Urabe, and I.\u00a0Hasuo. Tail probabilities for randomized program runtimes via martingales for higher moments. In T.\u00a0Vojnar and L.\u00a0Zhang, editors, Tools and Algorithms for the Construction and Analysis of Systems - 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part II, volume 11428 of Lecture Notes in Computer Science, pages 135\u2013153. Springer, 2019","DOI":"10.1007\/978-3-030-17465-1_8"},{"key":"10_CR41","unstructured":"M.\u00a0Z. Kwiatkowska, G.\u00a0Norman, and D.\u00a0Parker. PRISM 4.0: Verification of probabilistic real-time systems. In G.\u00a0Gopalakrishnan and S.\u00a0Qadeer, editors, Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings, volume 6806 of Lecture Notes in Computer Science, pages 585\u2013591. Springer, 2011"},{"key":"10_CR42","doi-asserted-by":"crossref","unstructured":"C.\u00a0Mak, C.\u00a0L. Ong, H.\u00a0Paquet, and D.\u00a0Wagner. Densities of almost surely terminating probabilistic programs are differentiable almost everywhere. In N.\u00a0Yoshida, editor, Programming Languages and Systems - 30th European Symposium on Programming, ESOP 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, volume 12648 of Lecture Notes in Computer Science, pages 432\u2013461. Springer, 2021","DOI":"10.1007\/978-3-030-72019-3_16"},{"key":"10_CR43","unstructured":"C.\u00a0Mak, F.\u00a0Zaiser, and L.\u00a0Ong. Nonparametric hamiltonian monte carlo. In M.\u00a0Meila and T.\u00a0Zhang, editors, Proceedings of the 38th International Conference on Machine Learning, volume 139 of Proceedings of Machine Learning Research, pages 7336\u20137347. PMLR, 18\u201324 Jul 2021"},{"key":"10_CR44","doi-asserted-by":"crossref","unstructured":"A.\u00a0McIver and C.\u00a0Morgan. Abstraction, Refinement and Proof for Probabilistic Systems. Monographs in Computer Science. Springer, 2005","DOI":"10.1145\/1059816.1059824"},{"key":"10_CR45","doi-asserted-by":"crossref","unstructured":"M.\u00a0Moosbrugger, E.\u00a0Bartocci, J.\u00a0Katoen, and L.\u00a0Kov\u00e1cs. Automated termination analysis of polynomial probabilistic programs. In N.\u00a0Yoshida, editor, Programming Languages and Systems - 30th European Symposium on Programming, ESOP 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, volume 12648 of Lecture Notes in Computer Science, pages 491\u2013518. Springer, 2021","DOI":"10.1007\/978-3-030-72019-3_18"},{"key":"10_CR46","doi-asserted-by":"crossref","unstructured":"M.\u00a0Moosbrugger, E.\u00a0Bartocci, J.\u00a0Katoen, and L.\u00a0Kov\u00e1cs. The probabilistic termination tool amber. In M.\u00a0Huisman, C.\u00a0S. Pasareanu, and N.\u00a0Zhan, editors, Formal Methods - 24th International Symposium, FM 2021, Virtual Event, November 20-26, 2021, Proceedings, volume 13047 of Lecture Notes in Computer Science, pages 667\u2013675. Springer, 2021","DOI":"10.1007\/978-3-030-90870-6_36"},{"issue":"OOPSLA2","key":"10_CR47","doi-asserted-by":"publisher","first-page":"1497","DOI":"10.1145\/3563341","volume":"6","author":"M Moosbrugger","year":"2022","unstructured":"Moosbrugger, M., Stankovic, M., Bartocci, E., Kov\u00e1cs, L.: This is the moment for probabilistic loops. Proc. ACM Program. Lang. 6(OOPSLA2), 1497\u20131525 (2022)","journal-title":"Proc. ACM Program. Lang."},{"key":"10_CR48","doi-asserted-by":"crossref","unstructured":"V.\u00a0C. Ngo, Q.\u00a0Carbonneaux, and J.\u00a0Hoffmann. Bounded expectations: resource analysis for probabilistic programs. In J.\u00a0S. Foster and D.\u00a0Grossman, editors, Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018, Philadelphia, PA, USA, June 18-22, 2018, pages 496\u2013512. ACM, 2018","DOI":"10.1145\/3192366.3192394"},{"issue":"3","key":"10_CR49","doi-asserted-by":"publisher","first-page":"969","DOI":"10.1512\/iumj.1993.42.42045","volume":"42","author":"M Putinar","year":"1993","unstructured":"Putinar, M.: Positive polynomials on compact semi-algebraic sets. Indiana Univ. Math. J. 42(3), 969\u2013984 (1993)","journal-title":"Indiana Univ. Math. J."},{"key":"10_CR50","doi-asserted-by":"crossref","unstructured":"T.\u00a0Quatmann and J.\u00a0Katoen. Sound value iteration. In H.\u00a0Chockler and G.\u00a0Weissenbacher, editors, Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part I, volume 10981 of Lecture Notes in Computer Science, pages 643\u2013661. Springer, 2018","DOI":"10.1007\/978-3-319-96145-3_37"},{"key":"10_CR51","unstructured":"T.\u00a0Rainforth. Automating inference, learning, and design using probabilistic programming. PhD thesis, University of Oxford, 2017"},{"key":"10_CR52","doi-asserted-by":"crossref","unstructured":"A.\u00a0\u015acibior, Z.\u00a0Ghahramani, and A.\u00a0D. Gordon. Practical probabilistic programming with monads. In B.\u00a0Lippmeier, editor, Proceedings of the 8th ACM SIGPLAN Symposium on Haskell, Haskell 2015, Vancouver, BC, Canada, September 3-4, 2015, pages 165\u2013176. ACM, 2015","DOI":"10.1145\/2804302.2804317"},{"key":"10_CR53","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1016\/j.tcs.2021.12.021","volume":"903","author":"M Stankovic","year":"2022","unstructured":"Stankovic, M., Bartocci, E., Kov\u00e1cs, L.: Moment-based analysis of bayesian network properties. Theor. Comput. Sci. 903, 113\u2013133 (2022)","journal-title":"Theor. Comput. Sci."},{"key":"10_CR54","doi-asserted-by":"crossref","unstructured":"T.\u00a0Takisaka, Y.\u00a0Oyabu, N.\u00a0Urabe, and I.\u00a0Hasuo. Ranking and repulsing supermartingales for reachability in randomized programs. ACM Trans. Program. Lang. Syst., 43(2):5:1\u20135:46, 2021","DOI":"10.1145\/3450967"},{"key":"10_CR55","unstructured":"J.\u00a0van\u00a0de Meent, B.\u00a0Paige, H.\u00a0Yang, and F.\u00a0Wood. An introduction to probabilistic programming. CoRR, abs\/1809.10756, 2018"},{"key":"10_CR56","doi-asserted-by":"crossref","unstructured":"D.\u00a0Wang, J.\u00a0Hoffmann, and T.\u00a0W. Reps. Central moment analysis for cost accumulators in probabilistic programs. In S.\u00a0N. Freund and E.\u00a0Yahav, editors, PLDI \u201921: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Virtual Event, Canada, June 20-25, 20211, pages 559\u2013573. ACM, 2021","DOI":"10.1145\/3453483.3454062"},{"key":"10_CR57","doi-asserted-by":"crossref","unstructured":"J.\u00a0Wang, Y.\u00a0Sun, H.\u00a0Fu, K.\u00a0Chatterjee, and A.\u00a0K. Goharshady. Quantitative analysis of assertion violations in probabilistic programs. In S.\u00a0N. Freund and E.\u00a0Yahav, editors, PLDI \u201921: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Virtual Event, Canada, June 20-25, 20211, pages 1171\u20131186. ACM, 2021","DOI":"10.1145\/3453483.3454102"},{"key":"10_CR58","doi-asserted-by":"crossref","unstructured":"P.\u00a0Wang, H.\u00a0Fu, A.\u00a0K. Goharshady, K.\u00a0Chatterjee, X.\u00a0Qin, and W.\u00a0Shi. Cost analysis of nondeterministic probabilistic programs. In K.\u00a0S. McKinley and K.\u00a0Fisher, editors, Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019, Phoenix, AZ, USA, June 22-26, 2019, pages 204\u2013220. ACM, 2019","DOI":"10.1145\/3314221.3314581"},{"key":"10_CR59","unstructured":"P.\u00a0Wang, H.\u00a0Fu, T.\u00a0Yang, G.\u00a0Li, and L.\u00a0Ong. Template-based static posterior inference for bayesian probabilistic programming. CoRR, abs\/2307.13160, 2023"},{"key":"10_CR60","doi-asserted-by":"crossref","unstructured":"D.\u00a0Williams. Probability with martingales. Cambridge University Press, 1991","DOI":"10.1017\/CBO9780511813658"}],"container-title":["Lecture Notes in Computer Science","Principles of Verification: Cycling the Probabilistic Landscape"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-75783-9_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,12]],"date-time":"2024-11-12T07:03:28Z","timestamp":1731395008000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-75783-9_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,11,13]]},"ISBN":["9783031757822","9783031757839"],"references-count":60,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-75783-9_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,11,13]]},"assertion":[{"value":"13 November 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}