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.

翻译：本文提出了一个面向离散概率程序的定量程序验证基础设施。该基础设施可被视为概率领域的Boogie：其核心组件包括一个中间验证语言（IVL）和一个实数值逻辑。我们的IVL提供了一种编程语言风格的表述验证条件的方式，这些条件的有效性蕴含了被研究程序的正确性。由于我们专注于验证定量属性，例如期望结果的上界、期望运行时间或终止概率，基于布尔一阶逻辑的现有IVL并不适用。相反，需要从标准布尔域向实数值域的范式转换。我们的IVL采用了对标准验证构造（如假设语句和断言语句）的定量推广。验证条件通过基于实数值逻辑的最弱前置条件语义生成。我们证明，该验证基础设施能够自然地编码文献中的多种验证技术。借助基于SMT的实现，我们自动验证了多种基准案例。据我们所知，这建立了首个针对概率程序期望推理的演绎验证基础设施。