| EPSRC Reference: |
EP/G069158/1 |
| Title: |
Automated Verification of Probabilistic Programs |
| Principal Investigator: |
Ouaknine, Professor J |
| Other Investigators: |
|
| 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 Date | Panel Name | Outcome |
|
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 |