The goal of this research is to demonstrate that probabilistic algorithms can be formally verified just like deterministic ones.
The key idea is to model a random number generator with an infinite sequence of bits; functions explicitly pass around this sequence as an extra parameter. When the algorithm needs to make a random choice, it pulls some bits off the sequence, and passes on the rest of the sequence. The question "What is the probability that this algorithm does X?" then becomes "What set of infinite bit sequences cause the algorithm to do X?" A formalization of mathematical measure theory is used to assign sets of infinite bit sequences a probability between 0 and 1.
This approach has been used to verify:
- sampling algorithms for four probability distributions;
- some optimal procedures for generating dice rolls from coin flips;
- the symmetric simple random walk; and
- the Miller-Rabin probabilistic primality test.
The algorithm that generates dice rolls from coin flips belongs to an interesting class that is not guaranteed to terminate, but nevertheless terminates with probability 1. For a simple example of this phenomenon consider repeatedly flipping a coin and stopping the first time it shows heads: if the coin shows tails forever you will never terminate, but this event occurs with probability 0. Formalizing this concept of probabilistic termination was necessary to verify interesting probabilistic algorithms.
- CANONICAL CITATION: Joe Hurd. Formal Verification of Probabilistic Algorithms. PhD thesis, University of Cambridge, 2002. [thesis] [bibtex] [talk]
- Joe Hurd, Annabelle McIver, and Carroll Morgan. Probabilistic guarded commands mechanized in HOL. Theoretical Computer Science, 346:96–112, November 2005. [paper] [bibtex] [talk]
- Joe Hurd. Verification of the Miller-Rabin probabilistic primality test. Journal of Logic and Algebraic Programming, 50(1–2):3–21, May–August 2003. Special issue on Probabilistic Techniques for the Design and Analysis of Systems. [paper] [bibtex] [talk]
- Joe Hurd. A formal approach to probabilistic termination. In Víctor A. Carreño, César A. Muñoz, and Sofiène Tahar, editors, 15th International Conference on Theorem Proving in Higher Order Logics: TPHOLs 2002, volume 2410 of Lecture Notes in Computer Science, pages 230–245, Hampton, VA, USA, August 2002. Springer. [paper] [bibtex] [talk]