一句话：提出用黎曼和近似积分，将连续概率程序的期望界验证归约为 SMT 不变量验证，并证明收敛与 coRE 完全性。
论文为连续概率程序的演绎验证奠定基础，目标是对含一般循环、连续分布与条件化的命令式概率程序，自动验证其期望结果的保证界。其关键思想是用黎曼和可靠地上下近似期望语义中的积分，使基于用户提供定量不变量的验证可借助 SMT 求解器完成，并适用于较一般的控制流。理论上，作者证明黎曼近似的收敛性，并给出核心验证问题的 coRE 完全性。实现上，在定量验证基础设施 Caesar 的中间验证语言中编码黎曼和，从而复用面向离散概率程序的自动验证器。若干案例研究初步展示了该方法的可行性。
We lay out novel foundations for the computer-aided verification of guaranteed bounds on expected outcomes of imperative probabilistic programs featuring (i) general loops , (ii) continuous distributions, and (iii) conditioning . To handle loops we rely on user-provided quantitative invariants , as is well established. However, in the realm of continuous distributions, invariant verification becomes extremely challenging due to the presence of integrals in expectation-based program semantics. Our key idea is to soundly under- or over-approximate these integrals via Riemann sums . We show that this approach enables the SMT-based invariant verification for programs with a fairly general control flow structure. On the theoretical side, we prove convergence of our Riemann approximations, and establish coRE-completeness of the central verification problems. On the practical side, we show that our approach enables to use existing automated verifiers targeting discrete probabilistic programs for the verification of programs involving continuous sampling . Towards this end, we implement our approach in the recent quantitative verification infrastructure Caesar by encoding Riemann sums in its intermediate verification language. We present several promising case studies.
@article{paperbot3169,
title = {Foundations for Deductive Verification of Continuous Probabilistic Programs: From Lebesgue to Riemann and Back},
author = {Kevin Batz and Joost-Pieter Katoen and Francesca Randone and Tobias Winkler},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA1},
year = {2025},
doi = {10.1145/3720429}
}