Details of Grant 

EPSRC Reference:	EP/D070880/1
Title:	A Unified Approach to Compositional Software Modelling, Analysis and Verification
Principal Investigator:	Ghica, Professor DR
Other Investigators:
Researcher Co-Investigators:
Project Partners:
Department:	School of Computer Science
Organisation:	University of Birmingham
Scheme:	Advanced Fellowship
Starts:	01 July 2006	Ends:	30 June 2011	Value (£):	386,160
EPSRC Research Topic Classifications:	Modelling & simul. of IT sys. Software Engineering
EPSRC Industrial Sector Classifications:	No relevance to Underpinning Sectors
Related Grants:
Panel History:	Panel Date Panel Name Outcome 25 Apr 2006 ICT Fellowships 2006 - Interview Panel Deferred 21 Mar 2006 ICT Fellowships 2006 - Sift Panel Deferred
Summary on Grant Application Form
Software modelling, analysis and verificationcomprises many sophisticated but often disparate techniques such asmodel checking, static analysis or testing. Although takenindividually such techniques are effective in targeting particularproblems, a combined approach is always recommended. However, in theabsence of a unified framework, integration can be awkward and mayfail to achieve true synergy. Using Game Semantics as a commontheoretical foundation we can provide such a unified framework forsoftware modelling, analysis and verification. The modularity ofextant techniques is often limited, which restrains theirscalability. Game Semantics is intrinsically compositional and recentresearch has already shown how it can be used to model subprograms inmodular fashion, especially the subtle interplay between proceduresand state that cannot be represented using extant techniques. However,compositional modelling is only the first step towards compositionalverification. We plan to further develop means for compositionalreasoning, that is methods of specifying properties of executionenvironments and of verifying that subprograms plug together withoutviolating their mutual assumptions. This can be achieved using eitherprogram logics or type systems. Building on existing research, we aimto push compositional methods beyond correctness verification, intomore intensional analyses such as estimating time of execution, memoryrequirements or resource usage. We also aim to expand beyond staticverification, by examining compositional approaches totesting. Throughout the programme, foundational and applied researchwill naturally intertwine and play off each other.
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.bham.ac.uk