| EPSRC Reference: |
GR/R85440/01 |
| Title: |
Code pointers and concurrency in spatial pointer logic |
| 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: |
16 July 2002 |
Ends: |
15 January 2003 |
Value (£): |
46,077
|
| EPSRC Research Topic Classifications: |
| Fundamentals of Computing |
|
|
| EPSRC Industrial Sector Classifications: |
| No relevance to Underpinning Sectors |
|
|
| Related Grants: |
|
| Panel History: |
|
|
Summary on Grant Application Form |
|
The purpose of this Visiting Fellowship application is to enable John Reynolds to visit Queen Mary from July-December in 2002. During this period we will build on our recent work on verifying programs that use dta pointers.. using our formalism of spatial pointer logic. The focus will be on open problems involving code pointers and concurrency. We aim to develop a reasoning method that addresses code pointers, demonstrating it on common instances such as stored code recursion of callback idioms. We also aim to extend our formalism of spatial pointer logic to deal with concurrency. Soundness of proof rules for monitors and conditional critical regions in the presence of heap memory.
|
|
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: |
|