{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T08:46:22Z","timestamp":1743065182934,"version":"3.40.3"},"publisher-location":"Cham","reference-count":58,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031757822"},{"type":"electronic","value":"9783031757839"}],"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_8","type":"book-chapter","created":{"date-parts":[[2024,11,12]],"date-time":"2024-11-12T07:02:02Z","timestamp":1731394922000},"page":"179-200","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Polar: An Algebraic Analyzer for\u00a0(Probabilistic) Loops"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2006-3741","authenticated-orcid":false,"given":"Marcel","family":"Moosbrugger","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0006-2909-2297","authenticated-orcid":false,"given":"Julian","family":"M\u00fcllner","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8004-6601","authenticated-orcid":false,"given":"Ezio","family":"Bartocci","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8299-2714","authenticated-orcid":false,"given":"Laura","family":"Kov\u00e1cs","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,11,13]]},"reference":[{"key":"8_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-030-81688-9_1","volume-title":"Computer Aided Verification","author":"A Abate","year":"2021","unstructured":"Abate, A., Giacobbe, M., Roy, D.: Learning probabilistic termination proofs. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12760, pp. 3\u201326. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81688-9_1"},{"key":"8_CR2","doi-asserted-by":"publisher","DOI":"10.1145\/3158122","author":"S Agrawal","year":"2018","unstructured":"Agrawal, S., Chatterjee, K., Novotn\u00fd, P.: Lexicographic ranking supermartingales: an efficient approach to termination of probabilistic programs. Proc. ACM Program. Lang. (POPL) (2018). https:\/\/doi.org\/10.1145\/3158122","journal-title":"Proc. ACM Program. Lang. (POPL)"},{"key":"8_CR3","doi-asserted-by":"publisher","DOI":"10.1145\/3434333","author":"A Aguirre","year":"2021","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. (POPL) (2021). https:\/\/doi.org\/10.1145\/3434333","journal-title":"Proc. ACM Program. Lang. (POPL)"},{"key":"8_CR4","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/978-3-031-22308-2_3","volume-title":"SAS 2022","author":"D Amrollahi","year":"2022","unstructured":"Amrollahi, D., Bartocci, E., Kenison, G., Kov\u00e1cs, L., Moosbrugger, M., Stankovic, M.: Solving invariant generation for unsolvable loops. In: Singh, G., Urban, C. (eds.) SAS 2022. LNCS, vol. 13790, pp. 19\u201343. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-22308-2_3"},{"key":"8_CR5","doi-asserted-by":"crossref","unstructured":"Amrollahi, D., Bartocci, E., Kenison, G., Kov\u00e1cs, L., Moosbrugger, M., Stankovic, M.: (Un)solvable loop analysis. Formal Methods Syst. Des. (2024, to appear)","DOI":"10.1007\/s10703-024-00455-0"},{"key":"8_CR6","doi-asserted-by":"publisher","DOI":"10.1145\/3428240","author":"M Avanzini","year":"2020","unstructured":"Avanzini, M., Moser, G., Schaper, M.: A modular cost analysis for probabilistic programs. Proc. ACM Program. Lang. (OOPSLA) (2020). https:\/\/doi.org\/10.1145\/3428240","journal-title":"Proc. ACM Program. Lang. (OOPSLA)"},{"key":"8_CR7","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/978-3-031-13185-1_3","volume-title":"CAV 2022","author":"J Bao","year":"2022","unstructured":"Bao, J., Trivedi, N., Pathak, D., Hsu, J., Roy, S.: Data-driven invariant learning for probabilistic programs. In: Shoham, S., Vizel, Y. (eds.) CAV 2022. LNCS, vol. 13371, pp. 33\u201354. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-13185-1_3"},{"key":"8_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-31113-0_1","volume-title":"Mathematics of Program Construction","author":"G Barthe","year":"2012","unstructured":"Barthe, G., Gr\u00e9goire, B., Zanella B\u00e9guelin, S.: Probabilistic relational hoare logics for computer-aided security proofs. In: Gibbons, J., Nogueira, P. (eds.) MPC 2012. LNCS, vol. 7342, pp. 1\u20136. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31113-0_1"},{"key":"8_CR9","doi-asserted-by":"publisher","unstructured":"Barthe, G., Katoen, J.P., Silva, A.: Foundations of Probabilistic Programming. Cambridge University Press (2020). https:\/\/doi.org\/10.1017\/9781108770750","DOI":"10.1017\/9781108770750"},{"key":"8_CR10","doi-asserted-by":"publisher","unstructured":"Barthe, G., K\u00f6pf, B., Olmedo, F., B\u00e9guelin, S.Z.: Probabilistic relational reasoning for differential privacy. In: Proceedings of POPL (2012). https:\/\/doi.org\/10.1145\/2103656.2103670","DOI":"10.1145\/2103656.2103670"},{"key":"8_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1007\/978-3-030-31784-3_15","volume-title":"Automated Technology for Verification and Analysis","author":"E Bartocci","year":"2019","unstructured":"Bartocci, E., Kov\u00e1cs, L., Stankovi\u010d, M.: Automatic generation of moment-based invariants for prob-solvable loops. In: Chen, Y.-F., Cheng, C.-H., Esparza, J. (eds.) ATVA 2019. LNCS, vol. 11781, pp. 255\u2013276. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-31784-3_15"},{"key":"8_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"492","DOI":"10.1007\/978-3-030-45190-5_28","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Bartocci","year":"2020","unstructured":"Bartocci, E., Kov\u00e1cs, L., Stankovi\u010d, M.: Mora - automatic generation of moment-based invariants. In: TACAS 2020. LNCS, vol. 12078, pp. 492\u2013498. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-45190-5_28"},{"key":"8_CR13","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"410","DOI":"10.1007\/978-3-031-30820-8_25","volume-title":"TACAS 2023","author":"K Batz","year":"2023","unstructured":"Batz, K., Chen, M., Junges, S., Kaminski, B.L., Katoen, J., Matheja, C.: Probabilistic program verification via inductive synthesis of inductive invariants. In: Sankaranarayanan, S., Sharygina, N. (eds.) TACAS 2023. LNCS, vol. 13994, pp. 410\u2013429. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-30820-8_25"},{"key":"8_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"524","DOI":"10.1007\/978-3-030-81688-9_25","volume-title":"Computer Aided Verification","author":"K Batz","year":"2021","unstructured":"Batz, K., Chen, M., Kaminski, B.L., Katoen, J.-P., Matheja, C., Schr\u00f6er, P.: Latticed k-induction with an application to probabilistic programs. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12760, pp. 524\u2013549. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81688-9_25"},{"key":"8_CR15","doi-asserted-by":"publisher","DOI":"10.1145\/3571260","author":"K Batz","year":"2023","unstructured":"Batz, K., Kaminski, B.L., Katoen, J., Matheja, C., Verscht, L.: A calculus for amortized expected runtimes. Proc. ACM Program. Lang. (POPL) (2023). https:\/\/doi.org\/10.1145\/3571260","journal-title":"Proc. ACM Program. Lang. (POPL)"},{"key":"8_CR16","doi-asserted-by":"publisher","unstructured":"Buchberger, B.: Bruno Buchberger\u2019s Phd thesis 1965: an algorithm for finding the basis elements of the residue class ring of a zero dimensional polynomial ideal. J. Symb. Comput. (2006). https:\/\/doi.org\/10.1016\/j.jsc.2005.09.007","DOI":"10.1016\/j.jsc.2005.09.007"},{"key":"8_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1007\/978-3-642-39799-8_34","volume-title":"Computer Aided Verification","author":"A Chakarov","year":"2013","unstructured":"Chakarov, A., Sankaranarayanan, S.: Probabilistic program analysis with martingales. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 511\u2013526. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_34"},{"key":"8_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-41528-4_1","volume-title":"Computer Aided Verification","author":"K Chatterjee","year":"2016","unstructured":"Chatterjee, K., Fu, H., Goharshady, A.K.: Termination analysis of probabilistic programs through Positivstellensatz\u2019s. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 3\u201322. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_1"},{"key":"8_CR19","doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Novotn\u00fd, P., Zikelic, D.: Stochastic invariants for probabilistic termination. In: Proceedings of POPL (2017). https:\/\/doi.org\/10.1145\/3009837.3009873","DOI":"10.1145\/3009837.3009873"},{"key":"8_CR20","doi-asserted-by":"publisher","unstructured":"Chen, J., He, F.: Proving almost-sure termination by omega-regular decomposition. In: Proceedings of PLDI (2020). https:\/\/doi.org\/10.1145\/3385412.3386002","DOI":"10.1145\/3385412.3386002"},{"key":"8_CR21","doi-asserted-by":"publisher","unstructured":"Chou, Y., Yoon, H., Sankaranarayanan, S.: Predictive runtime monitoring of vehicle models using Bayesian estimation and reachability analysis. In: Proceedings of IROS (2020). https:\/\/doi.org\/10.1109\/IROS45743.2020.9340755","DOI":"10.1109\/IROS45743.2020.9340755"},{"key":"8_CR22","doi-asserted-by":"publisher","unstructured":"Cox, D.A., Little, J., O\u2019Shea, D.: Ideals, Varieties, and Algorithms - An Introduction to Computational Algebraic Geometry and Commutative Algebra, 2nd edn. Springer, Cham (1997). https:\/\/doi.org\/10.1137\/1035171","DOI":"10.1137\/1035171"},{"key":"8_CR23","doi-asserted-by":"crossref","unstructured":"Everest, G., van\u00a0der Poorten, A.J., Shparlinski, I.E., Ward, T.: Recurrence Sequences. Mathematical Surveys and Monographs. American Mathematical Society, Providence (2003). ISBN 978-0-8218-3387-2","DOI":"10.1090\/surv\/104"},{"key":"8_CR24","doi-asserted-by":"publisher","unstructured":"Farzan, A., Kincaid, Z.: Compositional recurrence analysis. In: Proceedings of FMCAD (2015). https:\/\/doi.org\/10.1109\/FMCAD.2015.7542253","DOI":"10.1109\/FMCAD.2015.7542253"},{"key":"8_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"400","DOI":"10.1007\/978-3-319-68167-2_26","volume-title":"Automated Technology for Verification and Analysis","author":"Y Feng","year":"2017","unstructured":"Feng, Y., Zhang, L., Jansen, D.N., Zhan, N., Xia, B.: Finding polynomial loop invariants for probabilistic programs. In: D\u2019Souza, D., Narayan Kumar, K. (eds.) ATVA 2017. LNCS, vol. 10482, pp. 400\u2013416. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-68167-2_26"},{"key":"8_CR26","doi-asserted-by":"publisher","DOI":"10.1038\/nature14541","author":"Z Ghahramani","year":"2015","unstructured":"Ghahramani, Z.: Probabilistic machine learning and artificial intelligence. Nature (2015). https:\/\/doi.org\/10.1038\/nature14541","journal-title":"Nature"},{"key":"8_CR27","doi-asserted-by":"publisher","DOI":"10.1145\/3371105","author":"M Hark","year":"2020","unstructured":"Hark, M., Kaminski, B.L., Giesl, J., Katoen, J.: Aiming low is harder: induction for lower bounds in probabilistic program verification. Proc. ACM Program. Lang. (POPL) (2020). https:\/\/doi.org\/10.1145\/3371105","journal-title":"Proc. ACM Program. Lang. (POPL)"},{"key":"8_CR28","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/978-3-319-96812-4_10","volume-title":"Intelligent Computer Mathematics","author":"A Humenberger","year":"2018","unstructured":"Humenberger, A., Jaroschek, M., Kov\u00e1cs, L.: Aligator.jl \u2013 a Julia package for loop invariant generation. In: Rabe, F., Farmer, W.M., Passmore, G.O., Youssef, A. (eds.) CICM 2018. LNCS (LNAI), vol. 11006, pp. 111\u2013117. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96812-4_10"},{"key":"8_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"226","DOI":"10.1007\/978-3-319-73721-8_11","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A Humenberger","year":"2018","unstructured":"Humenberger, A., Jaroschek, M., Kov\u00e1cs, L.: Invariant generation for multi-path loops with polynomial assignments. In: VMCAI 2018. LNCS, vol. 10747, pp. 226\u2013246. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-73721-8_11"},{"key":"8_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/978-3-662-49498-1_15","volume-title":"Programming Languages and Systems","author":"BL Kaminski","year":"2016","unstructured":"Kaminski, B.L., Katoen, J.-P., Matheja, C., Olmedo, F.: Weakest precondition reasoning for expected run\u2013times of probabilistic programs. In: Thiemann, P. (ed.) ESOP 2016. LNCS, vol. 9632, pp. 364\u2013389. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49498-1_15"},{"key":"8_CR31","doi-asserted-by":"publisher","DOI":"10.1145\/3208102","author":"BL Kaminski","year":"2018","unstructured":"Kaminski, B.L., Katoen, J., Matheja, C., Olmedo, F.: Weakest precondition reasoning for expected runtimes of randomized algorithms. J. ACM (2018). https:\/\/doi.org\/10.1145\/3208102","journal-title":"J. ACM"},{"key":"8_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"390","DOI":"10.1007\/978-3-642-15769-1_24","volume-title":"Static Analysis","author":"J-P Katoen","year":"2010","unstructured":"Katoen, J.-P., McIver, A.K., Meinicke, L.A., Morgan, C.C.: Linear-invariant generation for probabilistic programs. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 390\u2013406. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15769-1_24"},{"key":"8_CR33","doi-asserted-by":"publisher","DOI":"10.1016\/j.peva.2010.04.001","author":"J Katoen","year":"2011","unstructured":"Katoen, J., Zapreev, I.S., Hahn, E.M., Hermanns, H., Jansen, D.N.: The ins and outs of the probabilistic model checker MRMC. Perform. Eval. (2011). https:\/\/doi.org\/10.1016\/j.peva.2010.04.001","journal-title":"Perform. Eval."},{"key":"8_CR34","unstructured":"Kauers, M.: Algorithms for nonlinear higher order difference equations. Ph.D. thesis, RISC, Johannes Kepler University, Linz (2005)"},{"key":"8_CR35","doi-asserted-by":"publisher","unstructured":"Kauers, M., Nuspl, P., Pillwein, V.: Order bounds for C2-finite sequences. In: Proceedings of ISSAC (2023). https:\/\/doi.org\/10.1145\/3597066.3597070","DOI":"10.1145\/3597066.3597070"},{"key":"8_CR36","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-7091-0445-3","volume-title":"The Concrete Tetrahedron - Symbolic Sums, Recurrence Equations, Generating Functions, Asymptotic Estimates","author":"M Kauers","year":"2011","unstructured":"Kauers, M., Paule, P.: The Concrete Tetrahedron - Symbolic Sums, Recurrence Equations, Generating Functions, Asymptotic Estimates. Springer, Vienna (2011). https:\/\/doi.org\/10.1007\/978-3-7091-0445-3"},{"key":"8_CR37","doi-asserted-by":"publisher","DOI":"10.1145\/3158142","author":"Z Kincaid","year":"2018","unstructured":"Kincaid, Z., Cyphert, J., Breck, J., Reps, T.W.: Non-linear reasoning for invariant synthesis. Proc. ACM Program. Lang. (POPL) (2018). https:\/\/doi.org\/10.1145\/3158142","journal-title":"Proc. ACM Program. Lang. (POPL)"},{"key":"8_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1007\/978-3-030-68446-4_12","volume-title":"Logic-Based Program Synthesis and Transformation","author":"L Klinkenberg","year":"2021","unstructured":"Klinkenberg, L., Batz, K., Kaminski, B.L., Katoen, J.-P., Moerman, J., Winkler, T.: Generating functions for probabilistic programs. In: LOPSTR 2020. LNCS, vol. 12561, pp. 231\u2013248. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-68446-4_12"},{"key":"8_CR39","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-031-16336-4_1","volume-title":"QEST 2022","author":"A Kofnov","year":"2022","unstructured":"Kofnov, A., Moosbrugger, M., Stankovic, M., Bartocci, E., Bura, E.: Moment-based invariants for probabilistic loops with non-polynomial assignments. In: \u00c1brah\u00e1m, E., Paolieri, M. (eds.) QEST 2022. LNCS, vol. 13479, pp. 3\u201325. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-16336-4_1"},{"key":"8_CR40","doi-asserted-by":"publisher","unstructured":"Kofnov, A., Moosbrugger, M., Stankovi\u010d, M., Bartocci, E., Bura, E.: Exact and approximate moment derivation for probabilistic loops with non-polynomial assignments. ACM Trans. Model. Comput. Simul. (2024, just Accepted). https:\/\/doi.org\/10.1145\/3641545","DOI":"10.1145\/3641545"},{"key":"8_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/978-3-540-78800-3_18","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Kov\u00e1cs","year":"2008","unstructured":"Kov\u00e1cs, L.: Reasoning algebraically about P-solvable loops. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 249\u2013264. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_18"},{"key":"8_CR42","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(85)90012-1","author":"D Kozen","year":"1985","unstructured":"Kozen, D.: A probabilistic PDL. J. Comput. Syst. Sci. (1985). https:\/\/doi.org\/10.1016\/0022-0000(85)90012-1","journal-title":"J. Comput. Syst. Sci."},{"key":"8_CR43","doi-asserted-by":"publisher","DOI":"10.1007\/b138392","volume-title":"Abstraction, Refinement and Proof for Probabilistic Systems","author":"A McIver","year":"2005","unstructured":"McIver, A., Morgan, C.: Abstraction, Refinement and Proof for Probabilistic Systems. Springer, New York (2005). https:\/\/doi.org\/10.1007\/b138392"},{"key":"8_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1007\/978-3-030-72016-2_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"F Meyer","year":"2021","unstructured":"Meyer, F., Hark, M., Giesl, J.: Inferring expected runtimes of probabilistic integer programs using expected sizes. In: TACAS 2021. LNCS, vol. 12651, pp. 250\u2013269. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-72016-2_14"},{"key":"8_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1007\/978-3-030-72019-3_18","volume-title":"Programming Languages and Systems","author":"M Moosbrugger","year":"2021","unstructured":"Moosbrugger, M., Bartocci, E., Katoen, J.-P., Kov\u00e1cs, L.: Automated termination analysis of polynomial probabilistic programs. In: ESOP 2021. LNCS, vol. 12648, pp. 491\u2013518. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-72019-3_18"},{"key":"8_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"667","DOI":"10.1007\/978-3-030-90870-6_36","volume-title":"Formal Methods","author":"M Moosbrugger","year":"2021","unstructured":"Moosbrugger, M., Bartocci, E., Katoen, J.-P., Kov\u00e1cs, L.: The probabilistic termination tool amber. In: Huisman, M., P\u0103s\u0103reanu, C., Zhan, N. (eds.) FM 2021. LNCS, vol. 13047, pp. 667\u2013675. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-90870-6_36"},{"key":"8_CR47","doi-asserted-by":"publisher","DOI":"10.1007\/S10703-023-00424-Z","author":"M Moosbrugger","year":"2022","unstructured":"Moosbrugger, M., Bartocci, E., Katoen, J., Kov\u00e1cs, L.: The probabilistic termination tool amber. Formal Methods Syst. Des. (2022). https:\/\/doi.org\/10.1007\/S10703-023-00424-Z","journal-title":"Formal Methods Syst. Des."},{"key":"8_CR48","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-031-47705-8_2","volume-title":"iFM 2023","author":"M Moosbrugger","year":"2023","unstructured":"Moosbrugger, M., M\u00fcllner, J., Kov\u00e1cs, L.: Automated sensitivity analysis for probabilistic loops. In: Herber, P., Wijs, A. (eds.) iFM 2023. LNCS, vol. 14300, pp. 21\u201339. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-47705-8_2"},{"key":"8_CR49","doi-asserted-by":"publisher","unstructured":"Moosbrugger, M., Stankovic, M., Bartocci, E., Kov\u00e1cs, L.: This is the moment for probabilistic loops. Proc. ACM Program. Lang. (OOPSLA2) (2022). https:\/\/doi.org\/10.1145\/3563341","DOI":"10.1145\/3563341"},{"key":"8_CR50","doi-asserted-by":"publisher","unstructured":"Motwani, R., Raghavan, P.: Randomized Algorithms. Cambridge University Press (1995). https:\/\/doi.org\/10.1017\/cbo9780511814075","DOI":"10.1017\/cbo9780511814075"},{"key":"8_CR51","doi-asserted-by":"publisher","DOI":"10.1145\/3632872","author":"J M\u00fcllner","year":"2024","unstructured":"M\u00fcllner, J., Moosbrugger, M., Kov\u00e1cs, L.: Strong invariants are hard: on the hardness of strongest polynomial invariants for (probabilistic) programs. Proc. ACM Program. Lang. (POPL) (2024). https:\/\/doi.org\/10.1145\/3632872","journal-title":"Proc. ACM Program. Lang. (POPL)"},{"key":"8_CR52","doi-asserted-by":"publisher","unstructured":"Ngo, V.C., Carbonneaux, Q., Hoffmann, J.: Bounded expectations: resource analysis for probabilistic programs. In: Proceedings of PLDI (2018). https:\/\/doi.org\/10.1145\/3192366.3192394","DOI":"10.1145\/3192366.3192394"},{"key":"8_CR53","doi-asserted-by":"publisher","unstructured":"Rodr\u00edguez-carbonell, E., Kapur, D.: Automatic generation of polynomial loop invariants: algebraic foundations. In: Proceedings of ISSAC (2004). https:\/\/doi.org\/10.1145\/1005285.1005324","DOI":"10.1145\/1005285.1005324"},{"key":"8_CR54","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2007.01.002","author":"E Rodr\u00edguez-Carbonell","year":"2007","unstructured":"Rodr\u00edguez-Carbonell, E., Kapur, D.: Generating all polynomial invariants in simple loops. J. Symb. Comput. (2007). https:\/\/doi.org\/10.1016\/j.jsc.2007.01.002","journal-title":"J. Symb. Comput."},{"key":"8_CR55","doi-asserted-by":"publisher","unstructured":"Schr\u00f6er, P., Batz, K., Kaminski, B.L., Katoen, J., Matheja, C.: A deductive verification infrastructure for probabilistic programs. Proc. ACM Program. Lang. (OOPSLA2) (2023). https:\/\/doi.org\/10.1145\/3622870","DOI":"10.1145\/3622870"},{"key":"8_CR56","doi-asserted-by":"publisher","unstructured":"Selyunin, K., Ratasich, D., Bartocci, E., Islam, M.A., Smolka, S.A., Grosu, R.: Neural programming: towards adaptive control in cyber-physical systems. In: Proceedings of CDC (2015). https:\/\/doi.org\/10.1109\/CDC.2015.7403319","DOI":"10.1109\/CDC.2015.7403319"},{"key":"8_CR57","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2021.12.021","author":"M Stankovic","year":"2022","unstructured":"Stankovic, M., Bartocci, E., Kov\u00e1cs, L.: Moment-based analysis of Bayesian network properties. Theor. Comput. Sci. (2022). https:\/\/doi.org\/10.1016\/j.tcs.2021.12.021","journal-title":"Theor. Comput. Sci."},{"key":"8_CR58","doi-asserted-by":"crossref","unstructured":"Tao, T.: Structure and Randomness. American Mathematical Society (2008). ISBN 0-8218-4695-7","DOI":"10.1090\/mbk\/059"}],"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_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,12]],"date-time":"2024-11-12T07:03:39Z","timestamp":1731395019000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-75783-9_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,11,13]]},"ISBN":["9783031757822","9783031757839"],"references-count":58,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-75783-9_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"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"}}]}}