EPSRC logo

Details of Grant 

EPSRC Reference: GR/R17034/01
Title: Local Reasoning About State
Principal Investigator: O'Hearn, Professor P
Other Investigators:
Bornat, Professor R Pym, Professor D
Researcher Co-Investigators:
Project Partners:
Department: Computer Science
Organisation: Queen Mary University of London
Scheme: Standard Research (Pre-FEC)
Starts: 01 March 2001 Ends: 29 February 2004 Value (£): 149,856
EPSRC Research Topic Classifications:
Fundamentals of Computing
EPSRC Industrial Sector Classifications:
No relevance to Underpinning Sectors
Related Grants:
Panel History:
Panel DatePanel NameOutcome
18 Oct 2000 Software Technologies Responsive Mode Deferred
Summary on Grant Application Form
In this research we propose an attack on the local reasoning problem: ideally, a specification and proof should be focused on a circumscribed collection of resources that a program actually acts upon, and not the enture conceivable state space of a system. We will approach this with a collection of semantic and logical tools developed by us and others, which appear to be well suited to the problem. Primary among these are: 1. Spatial possible world semantics, which works by breaking the state into components that different parts of a program act upon; and 2. Bunched Implications, a new substructural logic which contains logical primitives that enable spatial possible words to be exploited. Using these techniques, we will investigate challenging problems in program logic, especially reasoning about pointers. We will also develop an abstract framework, based on labelled transition systems. In each case we will prove the soundness of laws that enable local reasoning, and demonstrate their effectiveness by verifying example programs.
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: