|
| EPSRC Reference: |
EP/G069158/1 |
| Title: |
Automated Verification of Probabilistic Programs |
| Principal Investigator: |
Dr J Ouaknine |
| Other Investigators: |
|
| Researcher Co-investigator: |
|
| Project Partner: |
|
| Department: |
Computing Laboratory |
| Organisation: |
University of Oxford |
| Scheme: |
Standard Research |
| Starts: |
01 November 2009 |
Ends: |
30 April 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 Date | Panel Name | Outcome |
|
02 Jun 2009
|
ICT Prioritisation Panel (June 09)
|
Announced
|
|
|
Summary |
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.
|
| Final Report Summary |
|
No final report summary is available for this grant.
|
| Further Information: |
|
| Organisation Website: |
http://www.ox.ac.uk |
|
|