| EPSRC Reference: |
EP/K040863/1 |
| Title: |
Automating Separation Logic Reasoning |
| Principal Investigator: |
Navarro Perez, Dr J |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Computer Science |
| Organisation: |
UCL |
| Scheme: |
First Grant - Revised 2009 |
| Starts: |
01 January 2014 |
Ends: |
30 June 2015 |
Value (£): |
98,055
|
| EPSRC Research Topic Classifications: |
| Fundamentals of Computing |
|
|
| EPSRC Industrial Sector Classifications: |
|
| Related Grants: |
|
| Panel History: |
|
|
Summary on Grant Application Form |
Separation logic is a formalism designed to symbolically reason about computer programs that dynamically allocate data structures on memory. It allows to one mathematically _prove_ the correctness of such programs, for example showing the absence of memory leaks or violations. Using this proof system theoreticians could provide much cleaner and succinct proofs on the whiteboard, but their efforts to automate such reasoning process faced a number of limitations. Standard automated theorem proving techniques, based e.g. on resolution, did not seem to naturally apply to the new logic; thus researchers opted either to implement reasoning tools from scratch---missing the opportunity to exploit advances in modern theorem proving---or seek alternatives that avoid the perceived nuances of separation logic altogether---missing the conceptual advantages that separation logic _does_ provide. This research proposal seeks to demonstrate that modern theorem proving techniques are, in fact, compatible with separation logic reasoning. An approach that leads not only to much more efficient separation logic reasoners, but also broadens the scope of applications in which automated theorem proving can be practically applied.
|
|
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: |
|