Essential tasks for the verification of probabilistic programs include bounding expected outcomes and proving termination in finite expected runtime. We contribute a simple yet effective inductive synthesis approach for proving such quantitative reachability properties by generating inductive invariants on source-code level. Our implementation shows promise: It finds invariants for (in)finite-state programs, can beat state-of-the-art probabilistic model checkers, and is competitive with modern tools dedicated to invariant synthesis and expected runtime reasoning.

翻译：概率性程序验证的核心任务包括界定期望结果的上界以及证明其在有限期望运行时内的终止性。本文提出了一种简洁而高效的归纳合成方法，通过生成源代码级别的归纳不变量来证明此类定量可达性性质。我们的实现展现出良好前景：该方法能够为（有/无）限状态程序寻找不变量，其性能可超越当前最先进的概率模型检测工具，并与专攻不变量合成与期望运行时推理的现代工具具备竞争力。