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

TL;DR

This paper develops a new foundation for verifying expected outcomes of continuous probabilistic programs with loops and conditioning, using Riemann sums to approximate integrals and enabling SMT-based verification.

Contribution

It introduces a novel approach to handle continuous distributions in probabilistic programs via Riemann sum approximations, bridging Lebesgue and Riemann integration for verification.

Findings

Proves convergence of Riemann sum approximations for expectations.

Establishes coRE-completeness of verification problems.

Demonstrates practical verification using existing tools with case studies.

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.