Verifying Sampling Algorithms via Distributional Invariants

Lecture notes in computer science, pp. 259–278

Abstract

Abstract This paper presents a Hoare-like verification framework for discrete probabilistic programs that we apply to two non-trivial sampling algorithms: Lumbroso’s Fast Dice Roller and Saad et al.’s Fast Loaded Dice Roller . These algorithms have previously resisted formal verification due to their probabilistic nature, intricate loop structure, and parametric input. Our approach complements existing proof rules based on inductive distributional invariants, enabling us to verify both total and partial correctness of the two algorithms.

Authors 4

1. Daniel Zilken corresponding Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University, Aachen, Germany

2. Kevin Batz

   University College London

   Affiliation as printed

   University College London, London, UK

3. Joost-Pieter Katoen Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University, Aachen, Germany

4. Tobias Winkler Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University, Aachen, Germany