Automated Verification of Probabilistic Programs

Since the 1970s it has been widely recognised that introducing randomisation in the design of algorithms can yield substantial benefits. Unfortunately, randomised algorithms and protocols are notoriously difficult to get right, let alone to analyse and prove correct. The aim of this project is to develop algorithms, techniques, and tools to enable engineers and researchers to design and reason about probabilistic systems. We will also tackle a number of complexity and computability questions that arise naturally in the context of our planned research.

One of the starting points for this proposal is the novel prototype tool APEX, an automated equivalence checker for simple probabilistic programs that was developed by us recently. APEX is based on  game semantics, a sophisticated mathematical theory of programming languages, and is able to faithfully translate programs into probabilistic automata, which are theoretical 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 associated probabilistic 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 that the verification tasks can be carried out efficiently. Another strand of the project will be a systematic study of 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 be carried out simultaneously with the development and expansion of our verification infrastructure. In the longer term, we expect that the algorithms and tools that we develop will become directly useful to system designers and programmers.