EPSRC logo

Details of Grant 

EPSRC Reference: EP/G069158/1
Title: Automated Verification of Probabilistic Programs
Principal Investigator: Ouaknine, Professor J
Other Investigators:
Worrell, Professor JB Murawski, Professor A
Researcher Co-Investigators:
Project Partners:
Department: Computer Science
Organisation: University of Oxford
Scheme: Standard Research
Starts: 01 November 2009 Ends: 31 October 2011 Value (£): 290,346
EPSRC Research Topic Classifications:
Fundamentals of Computing Software Engineering
EPSRC Industrial Sector Classifications:
No relevance to Underpinning Sectors
Related Grants:
Panel History:
Panel DatePanel NameOutcome
02 Jun 2009 ICT Prioritisation Panel (June 09) Announced
Summary on Grant Application Form
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.
Key Findings
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Potential use in non-academic contexts
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Impacts
Description This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Summary
Date Materialised
Sectors submitted by the Researcher
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Project URL:  
Further Information:  
Organisation Website: http://www.ox.ac.uk