Automated Verification of Probabilistic Programs

Since the 1970s it has been widely recognised that introducingrandomisation in the design of algorithms can yield substantialbenefits. Unfortunately, randomised algorithms and protocols arenotoriously difficult to get right, let alone to analyse and prove correct. The aim of this project is to develop algorithms, techniques, andtools to enable engineers and researchers to design and reason aboutprobabilistic systems. We will also tackle a number ofcomplexity and computability questions that arise naturally in thecontext of our planned research.One of the starting points for this proposal is the novel prototype toolAPEX, an automated equivalence checker for simple probabilisticprograms that was developed by us recently. APEX is based on game semantics, a sophisticated mathematicaltheory of programming languages, and is able to faithfullytranslate programs into probabilistic automata, which aretheoretical models of probabilistic computation. As a first step, the project aims to greatly expand, at both a practical and theoretical level, the current capabilities of our probabilistic verification framework. We will then develop new algorithms for checking the correctness of probabilistic programs, by analysing their associatedprobabilistic automata. This comprises the development of specification formalisms in which program properties can be expressed, as well as efficient methods for verifying that the properties are satisfied.We will also investigate techniques for making the automata representations of programs as compact as possible so thatthe verification tasks can be carried out efficiently.Another strand of the project will be a systematic studyof the theoretical issues that stem naturally from our investigations.We plan to evaluate the outcome of our work on a series of case studies, to becarried out simultaneously with the development and expansion of ourverification infrastructure. In the longer term, we expect that the algorithms andtools that we develop will become directly useful to system designers andprogrammers.