| EPSRC Reference: |
GR/R17034/01 |
| Title: |
Local Reasoning About State |
| Principal Investigator: |
O'Hearn, Professor P |
| Other Investigators: |
|
| 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 Date | Panel Name | Outcome |
|
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: |
|