| EPSRC Reference: |
EP/J019577/1 |
| Title: |
Game Semantics for Java Programs |
| Principal Investigator: |
Murawski, Professor A |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Computer Science |
| Organisation: |
University of Warwick |
| Scheme: |
Standard Research |
| Starts: |
31 March 2013 |
Ends: |
30 September 2015 |
Value (£): |
209,084
|
| 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 |
|
06 Jun 2012
|
EPSRC ICT Responsive Mode - Jun 2012
|
Announced
|
|
|
Summary on Grant Application Form |
Although software verification has made great strides in the last few decades, it is well understood that
there is still a significant gap between the need and the supply of verification methods and tools.
In particular, methods which enjoy high accuracy and can scale up to the size of realistic applications
are extremely rare.
In this situation, methods stemming from the field of denotational semantics, which studies mathematical
models of programs using elements of set theory and logic, seem naturally advantageous. The denotational
approach uniquely combines two desirable features: abstraction and compositionality. Abstraction means
that the analysis focusses only on the observable aspects of program behaviour and is therefore bound
to lead to concise models. On the other hand, compositionality allows for large verification tasks to be broken
into constituent parts, which can then be solved separately.
The aim of this project is to use game semantics in order to devise models, prototype methods and tools
for Java programs. Game semantics is a denotational theory describing computation as a game: a dialogue
between the program and its environment which follows their exchange of data during program execution.
Games strike a balance between abstract mathematical models and operational techniques. They precisely
capture observable program behaviour but also provide models which have concrete representations and
are therefore amenable to algorihmic reasoning and automation. As a result, games constitute a natural
candidate for a refined semantics on which to base program verification.
Research in game semantics has recently made an important breakthrough towards the modelling of realistic
programming languages, with the introduction of a novel strand of the theory called Nominal Game Semantics.
Nominal games pinpoint dynamic program behaviours involving the generation of new resources, such as
reference names, objects, channels, etc. Moreover, research in automata over infinite alphabets has produced
machines with the potential of standing as algorithmic counterparts to nominal games. These developments
place us in a powerful position to attack Java, a mainstream language featuring such dynamic generative effects.
Our goal is to make an important step in devising disciplined, systematic and automated methods that bear
the potential to address difficulties not tackled by the state of the art and eventually lead to the development
of better software.
|
|
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.warwick.ac.uk |