Foundations for Deductive Verification of Continuous Probabilistic Programs: From Lebesgue to Riemann and Back

Proceedings of the ACM on Programming Languages, vol. 9, pp. 421–448

Abstract

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.

Authors 4

1. Kevin Batz Aachen

   University College London · RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University, Aachen, Germany

   University College London, London, United Kingdom

2. Joost-Pieter Katoen Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University, Aachen, Germany

3. Francesca Randone

   University of Trieste

   Affiliation as printed

   University of Trieste, Trieste, Italy

4. Tobias Winkler Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University, Aachen, Germany