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.
翻译:我们描述Amber 工具, 用来以完全自动的方式证明和反驳用多数值算术终止一类概率和概率程序的方法。 Amber 将马丁格理论与无症状约束功能的特性结合起来,并采用宽松的现有概率终止证据规则, 以证明/ 否定概率循环的几乎肯定终止。 Amber 支持以符号常数参数和从共同概率分布中提取参数的程序。 我们的实验性比较提供了实际证据,证明Amber 的性能超过了现有最先进的工具。