The Probabilistic Termination Tool Amber

TL;DR

Amber is an automated tool that proves or refutes the termination of probabilistic programs with polynomial arithmetic using martingale theory and asymptotic bounds, outperforming existing tools.

Contribution

The paper introduces Amber, a fully automated probabilistic termination analysis tool combining martingale theory with asymptotic bounds, supporting symbolic parameters and common distributions.

Findings

Amber outperforms existing tools in experiments.

It can prove or disprove almost sure termination.

Supports symbolic parameters and standard distributions.

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 parameterized by symbolic constants and drawing from common probability distributions. Our experimental comparisons give practical evidence of Amber outperforming existing state-of-the-art tools.