The probabilistic termination tool amber

Formal Methods in System Design, vol. 61, pp. 90–109

Abstract

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.

Authors 4

1. Marcel Moosbrugger corresponding

   TU Wien

   Affiliation as printed

   TU Wien, Vienna, Austria

2. Ezio Bartocci

   TU Wien

   Affiliation as printed

   TU Wien, Vienna, Austria

3. Joost-Pieter Katoen Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University, Aachen, Germany

4. Laura Kovács

   TU Wien

   Affiliation as printed

   TU Wien, Vienna, Austria