Skip to main content

Verifying Probabilistic Programs: Three Easy Pieces

Joel Ouaknine ( Oxford University Computing Laboratory )
I will discuss some recent work on automated verification of probabilistic programs and randomised algorithms, using a simple procedural probabilistic programming language for which we have built an equivalence checker, called APEX. I will illustrate our approach with three non-trivial case studies: (i) Herman's self-stabilisation algorithm; (ii) an analysis of the average shape of binary search trees obtained by sequences of random insertions and deletions; and (iii) the problem of anonymity in the Dining Cryptographers protocol.

This is joint with Andrzej Murawski, Ben Worrell, and Axel Legay.

Share this: