Verifying Probabilistic Programs: Three Easy Pieces
Joel Ouaknine ( Oxford University Computing Laboratory )
- 16:30 18th November 2008 ( week 6, Michaelmas Term 2008 )Lecture Theatre B
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.
This is joint with Andrzej Murawski, Ben Worrell, and Axel Legay.