Oxford University Computing Laboratory
4pm Tuesday, 22nd September, 2009
Room 4.31/33, Informatics Forum
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, James Worrell, and Axel Legay.