一句话：提出首个面向概率程序的演绎验证基础设施，用实值逻辑、中间验证语言与最弱前置条件支持期望型性质的自动验证。
论文针对离散概率程序的定量性质验证问题，目标包括期望结果、期望运行时间和终止概率等界的推理。现有基于布尔一阶逻辑的中间验证语言无法胜任这类定量推理，因此作者提出概率版的 Boogie 式基础设施：核心是一个中间验证语言（IVL）和实值逻辑，并将 assume、assert 等验证构造定量化。验证条件由基于该实值逻辑的最弱前置条件式语义生成。作者表明该基础设施可自然编码文献中的多种验证技术，并给出基于 SMT 的实现，在多个基准上实现自动验证。据作者所知，这是首个面向概率程序期望型推理的演绎验证基础设施。
This paper presents a quantitative program verification infrastructure for discrete probabilistic programs. Our infrastructure can be viewed as the probabilistic analogue of Boogie: its central components are an intermediate verification language (IVL) together with a real-valued logic. Our IVL provides a programming-language-style for expressing verification conditions whose validity implies the correctness of a program under investigation. As our focus is on verifying quantitative properties such as bounds on expected outcomes, expected run-times, or termination probabilities, off-the-shelf IVLs based on Boolean first-order logic do not suffice. Instead, a paradigm shift from the standard Boolean to a real-valued domain is required. Our IVL features quantitative generalizations of standard verification constructs such as assume- and assert-statements. Verification conditions are generated by a weakest-precondition-style semantics, based on our real-valued logic. We show that our verification infrastructure supports natural encodings of numerous verification techniques from the literature. With our SMT-based implementation, we automatically verify a variety of benchmarks. To the best of our knowledge, this establishes the first deductive verification infrastructure for expectation-based reasoning about probabilistic programs.
@article{paperbot1859,
title = {A Deductive Verification Infrastructure for Probabilistic Programs},
author = {Philipp Schröer and Kevin Batz and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {OOPSLA2},
year = {2023},
doi = {10.1145/3622870}
}