EPSRC logo

Details of Grant 

EPSRC Reference: EP/J019577/1
Title: Game Semantics for Java Programs
Principal Investigator: Murawski, Professor A
Other Investigators:
Tzevelekos, Dr N
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 DatePanel NameOutcome
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
Description This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
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