Skip to content

Software Quality

Probabilistic program verification

Probabilistic program verification proves a bound on what a program that samples random values does on average: the expected value of a result, the probability of an outcome, or the expected running time. It is deductive verification whose specifications describe the distribution of a program's runs rather than a single run.

A randomized program often has no useful worst case. A random walk that steps up with probability ¼ and down with probability ¾ can, in the worst case, step up forever, yet it terminates with probability 1; a worst-case resource analysis finds no bound for it, while its expected number of iterations is finite (Ngo et al. 2018)1.

How it works

A pre- and postcondition in a probabilistic program logic is either a real-valued function or a predicate on distributions (Barthe et al. 2018)2:

  • Expectation-based. A pre- and postcondition is a real-valued function on states. The calculus of weakest pre-expectations over pGCL propagates that function backwards through the program until it is a function of the input. It handles nondeterministic choice alongside probabilistic choice.
  • Assertion-based. A pre- and postcondition is a Boolean predicate on the distribution of states, which can state several probabilities or expected values in one assertion. Ellora is a sound and relatively complete logic of this kind, with proof rules for loops and for calls to adversarial code (Barthe et al. 2018)2.

Automation follows the non-probabilistic pattern. Caesar compiles a specification into HeyVL, an intermediate verification language with quantitative versions of assume and assert, generates verification conditions in a real-valued logic by a weakest-precondition-style semantics, and discharges them with an SMT solver — the probabilistic analogue of Boogie. Proof rules from the literature — invariants, k-induction, martingale arguments for almost-sure termination — are encoded in that language rather than built into the verifier (Schröer et al. 2023)3.

What it catches

  • Wrong expected outcomes. A randomized algorithm whose output is correct with lower probability than its specification claims fails the proof.
  • Unbounded expected cost. A loop that terminates with probability 1 but has infinite expected running time cannot meet a finite runtime bound.
  • Non-termination with positive probability. A proof of almost-sure termination fails where some run diverges with nonzero probability.

It does not find a bug in a single run: a correct probabilistic program can still produce a bad outcome, with the bounded probability the proof allows.

Tools

  • Caesar — verifier for HeyVL with a pGCL front end; bounds on expected outcomes, expected runtimes and termination probabilities, discharged by SMT.
  • Absynth — automatic analysis that infers polynomial upper bounds on expected resource consumption, in many cases by off-the-shelf linear programming, and emits each bound as a derivation in a quantitative program logic (Ngo et al. 2018)1.
  • Ellora — assertion-based logic implemented inside the EasyCrypt proof assistant; proofs are interactive (Barthe et al. 2018)2.

When to use, when not

Use it where a randomized algorithm or protocol has a probabilistic specification that must hold for every input: a success probability, an expected number of retransmissions, an expected running time.

Don't use it for a system modeled as a finite Markov chain, where probabilistic model checking computes the probability without a hand-written invariant; or where the distribution is unknown and only runs can be observed, which is statistical testing.

Evidence

  • Expected-cost bounds. On 39 probabilistic programs and randomized algorithms, Absynth's bounds were often asymptotically tight with precise, sometimes optimal, constant factors; some were not asymptotically tight (Ngo et al. 2018)1.
  • Verification time. On benchmarks of 19 to 270 lines of HeyVL drawn from the literature, Caesar verified a program in 0.2 seconds on average and 2.3 seconds at most; one benchmark timed out at the 10-second limit (Schröer et al. 2023)3.

Classification

  • Quality dimensions: Functionality, Performance (bounds expected running time and expected resource consumption where no worst-case bound exists).
  • Area: Randomized algorithms, communication protocols that retry or back off at random, cryptographic constructions, and models written in a probabilistic programming language.
  • Guarantee: Mathematical — the bound holds for every input under the program's semantics, not for a sample of runs.

References

  1. Ngo, Van Chan, Quentin Carbonneaux, and Jan Hoffmann. 2018. "Bounded Expectations: Resource Analysis for Probabilistic Programs." Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2018), 496–512. https://doi.org/10.1145/3192366.3192394. ↩↩↩

  2. Barthe, Gilles, Thomas Espitau, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub. 2018. "An Assertion-Based Program Logic for Probabilistic Programs." Programming Languages and Systems (ESOP 2018), Lecture notes in computer science, vol. 10801: 117–44. https://doi.org/10.1007/978-3-319-89884-1_5. ↩↩↩

  3. Schröer, Philipp, Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja. 2023. "A Deductive Verification Infrastructure for Probabilistic Programs." Proceedings of the ACM on Programming Languages 7 (OOPSLA2): 2052–82. https://doi.org/10.1145/3622870. ↩↩