The probabilistic termination tool amber

Area of Science:

• Computer Science
• Automated Reasoning
• Probabilistic Programming

Background:

• Automated termination analysis is crucial for program correctness.
• Probabilistic programs introduce complexities in termination verification.
• Existing tools struggle with programs involving polynomial arithmetic.

Purpose of the Study:

• To introduce the Amber tool for automated termination analysis of probabilistic while-programs.
• To address the challenge of proving/disproving termination for programs with polynomial arithmetic.
• To provide a more effective solution compared to existing state-of-the-art tools.

Main Methods:

• Amber combines martingale theory with asymptotic bounding functions.
• It implements relaxed probabilistic termination proof rules.
• The tool handles symbolic constants and common probability distributions.

Main Results:

• Amber successfully proves and refutes termination for a class of probabilistic while-programs.
• Experimental comparisons demonstrate Amber's superior performance.
• The tool achieves automated verification in a fully automated manner.

Conclusions:

• Amber offers an effective automated solution for probabilistic program termination analysis.
• The tool's approach advances the field of automated reasoning for probabilistic systems.
• Amber provides practical advantages over existing state-of-the-art termination analysis tools.