糖心TV

Title: Verifying Probabilistic Programs: Three Easy Pieces

Abstract: 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.