APEX

I will present a new framework, called APEX, for verifying probabilistic programs. APEX takes as input programs written in a C-like language with probabilistic operations, and models these using game semantics. The key property of our approach is that contextual equivalence for programs is decidable. This talk will give a brief overview of the underlying theory but will focus mainly on three case studies: Herman's self-stabilisation algorithm, an analysis of the average shape of binary search trees obtained by certain sequences of random insertions and deletions, and the problem of anonymity in the Dining Cryptographers protocol.

This is joint work with Axel Legay, Andrzej Murawsk, and James Worrell.