一句话：提出无需序列极限、仅需有限次应用循环体语义的概率程序期望值与运行时间下界归纳验证规则。
概率程序验证中，期望值以及期望运行时间的上界已有较成熟方法，但下界更难。本文提出一个新的归纳规则，用于验证概率循环执行后随机变量期望值和期望运行时间的下界。该规则的特点是：验证候选下界时只需有限次地应用循环体语义，因而不必像以往许多规则那样求某个序列的极限，使下界证明更为简单。摘要未报告工具实现或实验评估，贡献主要在验证规则与理论层面。
We present a new inductive rule for verifying lower bounds on expected values of random variables after execution of probabilistic loops as well as on their expected runtimes. Our rule issimplein the sense that loop body semantics need to be applied only finitely often in order to verify that the candidates are indeed lower bounds. In particular, it is not necessary to find the limit of a sequence as in many previous rules.
@article{paperbot542,
title = {Aiming low is harder: induction for lower bounds in probabilistic program verification},
author = {Marcel Hark and Benjamin Lucien Kaminski and Jürgen Giesl and Joost-Pieter Katoen},
journal = {Proceedings of the ACM on Programming Languages},
volume = {4},
number = {POPL},
year = {2019},
doi = {10.1145/3371105}
}