{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T20:58:18Z","timestamp":1760043498563,"version":"3.37.3"},"reference-count":30,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2022,8,1]],"date-time":"2022-08-01T00:00:00Z","timestamp":1659312000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,5,10]],"date-time":"2023-05-10T00:00:00Z","timestamp":1683676800000},"content-version":"vor","delay-in-days":282,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100001821","name":"Vienna Science and Technology Fund","doi-asserted-by":"publisher","award":["ICT19-018"],"award-info":[{"award-number":["ICT19-018"]}],"id":[{"id":"10.13039\/501100001821","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["101002685","787914"],"award-info":[{"award-number":["101002685","787914"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100002428","name":"Austrian Science Fund","doi-asserted-by":"publisher","award":["W1255-N23"],"award-info":[{"award-number":["W1255-N23"]}],"id":[{"id":"10.13039\/501100002428","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100004729","name":"Technische Universit\u00e4t Wien","doi-asserted-by":"publisher","award":["SecInt"],"award-info":[{"award-number":["SecInt"]}],"id":[{"id":"10.13039\/501100004729","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2022,8]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We describe the <jats:sc>Amber<\/jats:sc> tool for proving and refuting the termination of a class of probabilistic while-programs with polynomial arithmetic, in a fully automated manner. <jats:sc>Amber<\/jats:sc> combines martingale theory with properties of asymptotic bounding functions and implements relaxed versions of existing probabilistic termination proof rules to prove\/disprove (positive) almost sure termination of probabilistic loops. <jats:sc>Amber<\/jats:sc> supports programs parametrized by symbolic constants and drawing from common probability distributions. Our experimental comparisons give practical evidence of <jats:sc>Amber<\/jats:sc> outperforming existing state-of-the-art tools.<\/jats:p>","DOI":"10.1007\/s10703-023-00424-z","type":"journal-article","created":{"date-parts":[[2023,5,11]],"date-time":"2023-05-11T08:01:35Z","timestamp":1683792095000},"page":"90-109","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["The probabilistic termination tool amber"],"prefix":"10.1007","volume":"61","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2006-3741","authenticated-orcid":false,"given":"Marcel","family":"Moosbrugger","sequence":"first","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-6143-1926","authenticated-orcid":false,"given":"Joost-Pieter","family":"Katoen","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":[[2023,5,10]]},"reference":[{"key":"424_CR1","doi-asserted-by":"publisher","DOI":"10.1038\/nature14541","author":"Z Ghahramani","year":"2015","unstructured":"Ghahramani Z (2015) Probabilistic machine learning and artificial intelligence. Nature. https:\/\/doi.org\/10.1038\/nature14541","journal-title":"Nature"},{"key":"424_CR2","doi-asserted-by":"publisher","DOI":"10.1017\/9781108770750","volume-title":"Foundations of probabilistic programming","author":"G Barthe","year":"2020","unstructured":"Barthe G, Katoen J-P, Silva A (2020) Foundations of probabilistic programming. Cambridge University Press, Cambridge. https:\/\/doi.org\/10.1017\/9781108770750"},{"key":"424_CR3","doi-asserted-by":"publisher","unstructured":"Esparza J, Gaiser A, Kiefer S (2012) Proving termination of probabilistic programs using patterns. In: Proceedings of CAV. https:\/\/doi.org\/10.1007\/978-3-642-31424-7_14","DOI":"10.1007\/978-3-642-31424-7_14"},{"key":"424_CR4","doi-asserted-by":"publisher","unstructured":"Chakarov A, Sankaranarayanan S (2013) Probabilistic program analysis with martingales. In: Proceedings of CAV. https:\/\/doi.org\/10.1007\/978-3-642-39799-8_34","DOI":"10.1007\/978-3-642-39799-8_34"},{"key":"424_CR5","doi-asserted-by":"publisher","unstructured":"Ferrer\u00a0Fioriti LLM, Hermanns H (2015) Probabilistic termination: soundness, completeness, and compositionality. In: Proceedings of POPL. https:\/\/doi.org\/10.1145\/2676726.2677001","DOI":"10.1145\/2676726.2677001"},{"key":"424_CR6","doi-asserted-by":"publisher","unstructured":"Chatterjee K, Fu H, Goharshady AK (2016) Termination analysis of probabilistic programs through positivstellensatz\u2019s. In: Proceedings of CAV. https:\/\/doi.org\/10.1007\/978-3-319-41528-4_1","DOI":"10.1007\/978-3-319-41528-4_1"},{"key":"424_CR7","doi-asserted-by":"publisher","unstructured":"Agrawal S, Chatterjee K, Novotn\u00fd P (2017) Lexicographic ranking supermartingales: an efficient approach to termination of probabilistic programs. In: Proceedings of POPL. https:\/\/doi.org\/10.1145\/3158122","DOI":"10.1145\/3158122"},{"key":"424_CR8","doi-asserted-by":"publisher","unstructured":"Chatterjee K, Novotn\u00fd P, Zikelic D Stochastic Invariants for Probabilistic Termination. In: Proc. of POPL (2017). https:\/\/doi.org\/10.1145\/3009837.3009873","DOI":"10.1145\/3009837.3009873"},{"key":"424_CR9","doi-asserted-by":"publisher","DOI":"10.1145\/3158121","author":"A McIver","year":"2018","unstructured":"McIver A, Morgan C, Kaminski BL, Katoen J-P (2018) A new proof rule for almost-sure termination. Proc ACM Program Lang. https:\/\/doi.org\/10.1145\/3158121","journal-title":"Proc ACM Program Lang"},{"key":"424_CR10","doi-asserted-by":"publisher","unstructured":"Huang M, Fu H, Chatterjee K (2018) New approaches for almost-sure termination of probabilistic programs. In: Proceedings of APLAS. https:\/\/doi.org\/10.1007\/978-3-030-02768-1_11","DOI":"10.1007\/978-3-030-02768-1_11"},{"key":"424_CR11","doi-asserted-by":"publisher","unstructured":"Chen J, He F (2020) Proving almost-sure termination by omega-regular decomposition. In: Proceedings of PLDI. https:\/\/doi.org\/10.1145\/3385412.3386002","DOI":"10.1145\/3385412.3386002"},{"key":"424_CR12","doi-asserted-by":"publisher","unstructured":"Chatterjee K, Goharshady AK, Meggendorfer T, Zikelic D (2022) Sound and complete certificates for quantitative termination analysis of probabilistic programs. In: Proceedings of CAV. https:\/\/doi.org\/10.1007\/978-3-031-13185-1_4","DOI":"10.1007\/978-3-031-13185-1_4"},{"key":"424_CR13","doi-asserted-by":"publisher","unstructured":"Bournez O, Garnier F (2005) Proving positive almost-sure termination. In: Proceedings of RTA. https:\/\/doi.org\/10.1007\/978-3-540-32033-3_24","DOI":"10.1007\/978-3-540-32033-3_24"},{"key":"424_CR14","doi-asserted-by":"publisher","unstructured":"Chatterjee K, Fu H, Novotn\u00fd P (2020) Termination analysis of probabilistic programs with martingales. Foundations of probabilistic programming. Cambridge University Press, Cambridge, pp 221\u2013258. https:\/\/doi.org\/10.1017\/9781108770750.008","DOI":"10.1017\/9781108770750.008"},{"key":"424_CR15","doi-asserted-by":"publisher","unstructured":"Ngo VC, Carbonneaux Q, Hoffmann J (2018) Bounded expectations: resource analysis for probabilistic programs. In: Proceedings of PLDI. https:\/\/doi.org\/10.1145\/3192366.3192394","DOI":"10.1145\/3192366.3192394"},{"key":"424_CR16","doi-asserted-by":"publisher","unstructured":"Meyer F, Hark M, Giesl J (2021) Inferring expected runtimes of probabilistic integer programs using expected sizes. In: Proceedings of TACAS. https:\/\/doi.org\/10.1007\/978-3-030-72016-2_14","DOI":"10.1007\/978-3-030-72016-2_14"},{"key":"424_CR17","doi-asserted-by":"publisher","unstructured":"Avanzini M, Moser G, Schaper M (2020) A modular cost analysis for probabilistic programs. In: Proceedings of OOPSLA. https:\/\/doi.org\/10.1145\/3428240","DOI":"10.1145\/3428240"},{"key":"424_CR18","doi-asserted-by":"publisher","unstructured":"Moosbrugger M, Bartocci E, Katoen J-P, Kov\u00e1cs L (2021) Automated termination analysis of polynomial probabilistic programs. In: Proceedings of ESOP. https:\/\/doi.org\/10.1007\/978-3-030-72019-3_18","DOI":"10.1007\/978-3-030-72019-3_18"},{"key":"424_CR19","doi-asserted-by":"publisher","unstructured":"Moosbrugger M, Bartocci E, Katoen JP, Kov\u00e1cs L (2021) The probabilistic termination tool amber. In: Proceedings of FM. https:\/\/doi.org\/10.1007\/978-3-030-90870-6_36","DOI":"10.1007\/978-3-030-90870-6_36"},{"key":"424_CR20","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4684-9455-6","volume-title":"Denumerable Markov chains: with a chapter of Markov random fields by David Griffeath","author":"JG Kemeny","year":"1976","unstructured":"Kemeny JG, Snell JL, Knapp AW (1976) Denumerable Markov chains: with a chapter of Markov random fields by David Griffeath. Springer, New York"},{"key":"424_CR21","doi-asserted-by":"publisher","DOI":"10.1017\/9781108591034","volume-title":"Probability: theory and examples","author":"R Durrett","year":"2019","unstructured":"Durrett R (2019) Probability: theory and examples. Cambridge University Press, Cambridge"},{"key":"424_CR22","series-title":"Mathematical Surveys Monograph","doi-asserted-by":"publisher","DOI":"10.1090\/surv\/104","volume-title":"Recurrence sequences","author":"G Everest","year":"2003","unstructured":"Everest G, van der Poorten A, Shparlinski I, Ward T (2003) Recurrence sequences. Mathematical Surveys Monograph. Amer. Math. Soc, Providence"},{"key":"424_CR23","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 (2011) The concrete tetrahedron: symbolic sums, recurrence equations, generating functions, asymptotic estimates. Springer, New York"},{"key":"424_CR24","doi-asserted-by":"publisher","unstructured":"Gruntz D (1996) On computing limits in a symbolic manipulation system. PhD thesis, ETH Z\u00fcrich. https:\/\/doi.org\/10.3929\/ETHZ-A-001631582","DOI":"10.3929\/ETHZ-A-001631582"},{"key":"424_CR25","doi-asserted-by":"publisher","unstructured":"Maritz MF (2020) A note on exact solutions of the logistic map. Chaos Interdiscip J Nonlinear Sci. https:\/\/doi.org\/10.1063\/1.5125097","DOI":"10.1063\/1.5125097"},{"key":"424_CR26","doi-asserted-by":"publisher","unstructured":"Bartocci E, Kov\u00e1cs L, Stankovic M (2020) Analysis of Bayesian networks via prob-solvable loops. In: Proceedings of ICTAC (2020). https:\/\/doi.org\/10.1007\/978-3-030-64276-1_12","DOI":"10.1007\/978-3-030-64276-1_12"},{"key":"424_CR27","doi-asserted-by":"publisher","unstructured":"Bartocci E, Kov\u00e1cs L, Stankovic M (2020) Mora\u2014automatic generation of moment-based invariants. In: Proceedings of TACAS. https:\/\/doi.org\/10.1007\/978-3-030-45190-5","DOI":"10.1007\/978-3-030-45190-5"},{"key":"424_CR28","doi-asserted-by":"publisher","unstructured":"Saheb-Djahromi N (1978) Probabilistic LCF In: Proceedings of MFCS. https:\/\/doi.org\/10.1007\/3-540-08921-7_92","DOI":"10.1007\/3-540-08921-7_92"},{"key":"424_CR29","doi-asserted-by":"publisher","unstructured":"Kaminski BL, Katoen JP (2015) On the hardness of almost-sure termination. In: Proceedings of MFCS. https:\/\/doi.org\/10.1007\/978-3-662-48057-1_24","DOI":"10.1007\/978-3-662-48057-1_24"},{"key":"424_CR30","doi-asserted-by":"publisher","unstructured":"Bartocci E, Kov\u00e1cs L, Stankovic M (2019) Automatic generation of moment-based invariants for prob-solvable loops. In: Proceedings of ATVA. https:\/\/doi.org\/10.1007\/978-3-030-31784-3_15","DOI":"10.1007\/978-3-030-31784-3_15"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-023-00424-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-023-00424-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-023-00424-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,11,30]],"date-time":"2023-11-30T15:10:07Z","timestamp":1701357007000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-023-00424-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,8]]},"references-count":30,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2022,8]]}},"alternative-id":["424"],"URL":"https:\/\/doi.org\/10.1007\/s10703-023-00424-z","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2022,8]]},"assertion":[{"value":"18 March 2022","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"16 April 2023","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"10 May 2023","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}