| EPSRC Reference: |
EP/G049920/1 |
| Title: |
Modular liveness proofs for concurrent programs |
| Principal Investigator: |
Gotsman, Mr O |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Computer Science and Technology |
| Organisation: |
University of Cambridge |
| Scheme: |
Postdoc Research Fellowship |
| Starts: |
01 November 2009 |
Ends: |
31 October 2010 |
Value (£): |
216,181
|
| EPSRC Research Topic Classifications: |
| Fundamentals of Computing |
|
|
| EPSRC Industrial Sector Classifications: |
|
| Related Grants: |
|
| Panel History: |
|
|
Summary on Grant Application Form |
|
Reasoning about concurrent programs is difficult because of the need to consider all possible interactions among concurrently executing threads. Modular reasoning techniques sidestep this difficulty by considering every thread in isolation under some assumptions on its environment. To date, such techniques have been largely limited to the verification of properties that guarantee the absence of bad events (safety properties). The available modular techniques do not deal well with the remaining set of properties, which ensure that good events eventually happen (liveness properties).The aim of the proposed research is to develop logics for modular reasoning about liveness and performance properties of concurrent programs and methods of automating proofs in them. The logics and the methods should be applicable to a wide range of programs, including those that use fine-grained or non-blocking synchronization.The proposed research, if successful, will build the foundations for developing efficient, yet reliable, concurrent systems. In time, its results may feed into industrial tools for software development and verification.
|
|
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 |