Quantitative Analysis of Assertion Violations in Probabilistic Programs

TL;DR

This paper introduces automated algorithms for deriving tight quantitative bounds on assertion violation probabilities in probabilistic programs, based on new fixed-point theorems and advanced mathematical tools.

Contribution

It presents the first automated methods for lower bounds and complete upper bounds on assertion violations, improving accuracy over prior stochastic invariant approaches.

Findings

Algorithms produce significantly tighter bounds than previous methods.

Successfully handle a wide variety of probabilistic programs.

Provide the first automated lower-bound algorithm for assertion violations.

Abstract

In this work, we consider the fundamental problem of deriving quantitative bounds on the probability that a given assertion is violated in a probabilistic program. We provide automated algorithms that obtain both lower and upper bounds on the assertion violation probability in exponential forms. The main novelty of our approach is that we prove new and dedicated fixed-point theorems which serve as the theoretical basis of our algorithms and enable us to reason about assertion violation bounds in terms of pre and post fixed-point functions. To synthesize such fixed-points, we devise algorithms that utilize a wide range of mathematical tools, including repulsing ranking super-martingales, Hoeffding's lemma, Minkowski decompositions, Jensen's inequality, and convex optimization. On the theoretical side, we provide (i) the first automated algorithm for lower-bounds on assertion violation probabilities, (ii) the first complete algorithm for upper-bounds of exponential form in affine programs, and (iii) provably and significantly tighter upper-bounds than the previous approach of stochastic invariants. On the practical side, we show that our algorithms can handle a wide variety of programs from the literature and synthesize bounds that are several orders of magnitude tighter in comparison with previous approaches.