Details of Grant 

EPSRC Reference:	EP/F019394/1
Title:	Modular verification of concurrent programs: Marrying Rely-Guarantee and Separation Logic
Principal Investigator:	Winskel, Professor G
Other Investigators:	Parkinson, Dr M
Researcher Co-Investigators:
Project Partners:
Department:	Computer Science and Technology
Organisation:	University of Cambridge
Scheme:	First Grant Scheme
Starts:	31 March 2008	Ends:	30 December 2011	Value (£):	259,563
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 19 Jul 2007 ICT Prioritisation Panel (Technology) Announced
Summary on Grant Application Form
Reasoning about concurrent programs is difficult because of the fantastic complexity of potential interactions between concurrent processes. These problems are set to distress many more programmers with the advance of multi-core processors, where several CPU's share a common store. In the quest for tractable methods for reasoning about concurrent algorithms both rely/guarantee logic and separation logic have made great advances. They both seek to tame, or control, the complexity of concurrent interactions, but neither is the ultimate approach. Rely-guarantee copes naturally with interference, but its specifications are complex because they describe the entire state. Conversely separation logic has difficulty dealing with interference, but specifications are simpler because they describe only the relevant state, that is its footprint. We propose a new logic, which marries their strengths but not their weaknesses. Our proposal involves both fundamental theoretical work on program logic and practical work on automatic verification for this logic. Success in this project will mean a significant step towards solving the long-standing open problem of tractable reasoning about concurrency.
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:	http://www.cam.ac.uk