| EPSRC Reference: |
GR/S53961/01 |
| Title: |
Local Reasoning: Foundations and Applications |
| Principal Investigator: |
O'Hearn, Professor P |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Computer Science |
| Organisation: |
Queen Mary University of London |
| Scheme: |
Advanced Fellowship (Pre-FEC) |
| Starts: |
01 October 2003 |
Ends: |
31 March 2009 |
Value (£): |
258,545
|
| 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 |
|
21 May 2003
|
IT Fellowships Interview Panel 2003
|
Deferred
|
|
25 Apr 2003
|
IT Fellowships Sift Panel 2003
|
Deferred
|
|
|
Summary on Grant Application Form |
|
Building on research on resource-oriented logics, particularly separation logic, we propose to develop a general theory local reasoning: ideally, reasoning and specifications should concentrate on the resources that a program actually accesses, and not the entire global state of a system. Our research has foundational and application components. Th foundations involve resource-centric accounts of information hiding and modularity, concurrency, distribution, code pointers, and an investigation of the abstract mathematical principles underlying local reasoning. Our applications wo organized around safe fundamental code as a focus problem. An outcome will be algorithms which check safety properties of low-level code that manages resources explicitly, analogous to the typechecking methods used in highe level languages. We will also develop verification technology for portions of code which cannot be automatically chec The overall aim is to provide a unified theory -- which has a conceptually and technically coherent form of locality buil at a base level; which covers a variety of models such as where the resources are memory addresses, files, semaphor process id's, communication channels, URLs, or simply portions of a data or knowledge base; and which forms the N for new applications, themselves exemplified by prototype implementations.
|
|
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: |
|