论文标题
概率的程序验证通过电感不变性的感应合成
Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants
论文作者
论文摘要
验证概率计划的基本任务包括在有限的预期运行时界定预期结果和证明终止。我们通过在源代码水平上产生电感不变性来证明一种简单而有效的电感合成方法来证明这种定量可达性能。我们的实施表明了承诺：它找到了（IN）有限状态程序的不变性，可以击败最先进的概率模型检查器，并且与专门用于不变综合和预期运行时推理的现代工具具有竞争力。
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.
