| EPSRC Reference: |
EP/D053625/1 |
| Title: |
Modularity and Resource Separation |
| 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 October 2006 |
Ends: |
30 June 2010 |
Value (£): |
266,116
|
| EPSRC Research Topic Classifications: |
| Fundamentals of Computing |
Software Engineering |
|
| EPSRC Industrial Sector Classifications: |
| No relevance to Underpinning Sectors |
|
|
| Related Grants: |
|
| Panel History: |
|
|
Summary on Grant Application Form |
|
Modularity is a key concept which programmers wield in their struggle againstthe complexity of software systems. When a program is divided into conceptually distinct modules or components, each of which uses separate internal resources (such as storage),the effort required for understanding the program is decomposed into circumscribed, hopefully manageable, parts. The purpose of this project is to bring separation logic to bear on modularity.The separating conjunction connective will be used to give a precise, theoretical expression that correspondsto the existing pre-formal, intuitive link between resource separation and modularity.We will develop semantic models that describe when a piece of state used by a module is held separate from the clients that use it. Theories of refinement and parametricity will be studied. The former will begin to address one of the common criticisms of separation logic,that verifications take place on a fixed (low) level of abstraction. The latter will give us methods for showing equivalence of imperative modules and for understanding information hiding for imperative resources. We will also investigate methods for proof and static checking and analysis for imperative modules. This project contribute considerably to the problems of scalable reasoning about programs and protection of resources from outside tampering, in the presence of practical programming features such as pointers thathave previously been seen as barriers to technically precise accounts of modularity.
|
|
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: |
|