# 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)[^ngo2018].

## 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)[^barthe2018]:

- **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)[^barthe2018].

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)[^schroer2023].

## 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](https://www.caesarverifier.org/)** — 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)[^ngo2018].
- **Ellora** — assertion-based logic implemented inside the EasyCrypt proof
  assistant; proofs are interactive (Barthe et al. 2018)[^barthe2018].

## 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](https://quality.stereobooster.com/probabilistic-model-checking.md) computes the
probability without a hand-written invariant; or where the distribution is
unknown and only runs can be observed, which is
[statistical testing](https://quality.stereobooster.com/statistical-testing.md).

## 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)[^ngo2018].
- **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)[^schroer2023].

## 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

[^ngo2018]: Ngo, Van Chan, Quentin Carbonneaux, and Jan Hoffmann. 2018. "[Bounded Expectations: Resource Analysis for Probabilistic Programs](https://arxiv.org/pdf/1711.08847)." *Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2018)*, 496–512. <https://doi.org/10.1145/3192366.3192394>.
[^barthe2018]: Barthe, Gilles, Thomas Espitau, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub. 2018. "[An Assertion-Based Program Logic for Probabilistic Programs](https://arxiv.org/pdf/1803.05535)." *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](https://doi.org/10.1007/978-3-319-89884-1\_5).
[^schroer2023]: Schröer, Philipp, Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja. 2023. "[A Deductive Verification Infrastructure for Probabilistic Programs](https://arxiv.org/pdf/2309.07781)." *Proceedings of the ACM on Programming Languages* 7 (OOPSLA2): 2052–82. <https://doi.org/10.1145/3622870>.

## Acronyms

- SMT — satisfiability modulo theories