Moosbrugger, M., Bartocci, E., Katoen, J.-P., & Kovacs, L. (2022). The probabilistic termination tool amber. Formal Methods in System Design, 61(1), 90–109. https://doi.org/10.1007/s10703-023-00424-z
We describe the Amber tool for proving and refuting the termination of a class of probabilistic while-programs with polynomial arithmetic, in a fully automated manner. Amber 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. Amber supports programs parametrized by symbolic constants and drawing from common probability distributions. Our experimental comparisons give practical evidence of Amber outperforming existing state-of-the-art tools.
en
Project title:
Distribution Recovery for Invariant Generation of Probabilistic Programs: ICT19-018 (WWTF Wiener Wissenschafts-, Forschu und Technologiefonds) Automated Reasoning with Theories and Induction for Software Technologies: ERC Consolidator Grant 2020 (European Commission)
-
Research Areas:
Logic and Computation: 50% Computer Engineering and Software-Intensive Systems: 50%
