| EPSRC Reference: |
EP/L022478/1 |
| Title: |
Program Reasoning with Nominal Game Semantics |
| Principal Investigator: |
Tzevelekos, Dr N |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Sch of Electronic Eng & Computer Science |
| Organisation: |
Queen Mary University of London |
| Scheme: |
First Grant - Revised 2009 |
| Starts: |
30 June 2014 |
Ends: |
29 December 2015 |
Value (£): |
100,228
|
| EPSRC Research Topic Classifications: |
| Fundamentals of Computing |
|
|
| EPSRC Industrial Sector Classifications: |
| No relevance to Underpinning Sectors |
|
|
| Related Grants: |
|
| Panel History: |
| Panel Date | Panel Name | Outcome |
|
04 Feb 2014
|
EPSRC ICT Responsive Mode - Feb 2014
|
Announced
|
|
|
Summary on Grant Application Form |
While in recent years great strides have been made in software verification, most of these successes have targeted programming languages of a strong imperative flavour. However, there is an emerging class of languages using higher-order features to cater for well-structured and disciplined programming outputs, for which verification methods are very scarce. In such higher-order languages, capturing formally the behaviour of programs is highly non-trivial and, therefore, even simple program analysis tasks prove to be surprisingly daunting.
This project will combine the latest techniques from game semantics with successful verification approaches from the imperative setting in order to achieve a novel reasoning methodology for higher-order languages. Game semantics is a theory of computation that has emerged as a robust paradigm for assigning formal mathematical semantics to higher-order programs. Game models offer a particularly suitable foundation for program analysis as they combine two features of focal importance: abstraction and compositionality. The former is achieved by focussing only on observable program behaviours, which significantly reduces the examined state-space of programs. The latter amounts to modelling compound program phrases by canonically combining the models of their respective sub-phrases, which in turn allows for the independent analysis of program components and enables local reasoning techniques.
The major obstacle in applying game semantics to real program analysis has been the modelling of dynamic generative effects, involving the generation of fresh references, objects, channels, etc. This issue has been addressed by a recent breakthrough that introduced atomic objects, called "names", in games for representing datatypes of dynamically generated resources. Names led to the introduction of a new strand of the theory called Nominal Game Semantics. Nominal games have extended the reach of game models to realistic higher-order languages and have brought the field to the point where one can start developing formal reasoning methods for such languages.
Our research will take the theory of game semantics to the next level and apply it to program reasoning. Our aim is to derive practical program logics for higher-order programs, equipped with high-level rules enabling abstraction and local reasoning, and complement them with a prototype implementation. The overall vision behind this proposal is to exploit the strong handle on higher-order computation provided by the nominal approach to game semantics in order to significantly extend the reach of modern approaches to verification and aid the production 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: |
|