| EPSRC Reference: |
GR/M75440/01 |
| Title: |
COMPOSITIONAL PROOFS OF CONCURRENT PROGRAMS |
| Principal Investigator: |
Paulson, Professor LC |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Computer Science and Technology |
| Organisation: |
University of Cambridge |
| Scheme: |
Standard Research (Pre-FEC) |
| Starts: |
17 January 2000 |
Ends: |
16 June 2003 |
Value (£): |
157,756
|
| EPSRC Research Topic Classifications: |
|
| EPSRC Industrial Sector Classifications: |
| Information Technologies |
No relevance to Underpinning Sectors |
|
| Related Grants: |
|
| Panel History: |
|
|
Summary on Grant Application Form |
|
UNITY is a formalism for proving the correctness of concurrent systems, both hardware and software. The proposal concerns proving the correctness of UNITY programs built from components that are specified and verified independently. The correctness proof should refer to the properties previously proved rather than regarding the composite system as one giant program. Writing F1 IG for the parallel composition of the two programs F and G, the goal is to derive properties of FJJG from abstract properties of F and G.We can reason in this compositional way about safety. If both F and G satisfy the same invariant, then so does F11G. However, such reasoning does not work for progress, either because F and G interfere with each other or because progress occurs only through their joint action.Several researchers, e.g Chandy, Charpentier, Misra and Sanders, have proposed methods for reasoning about compositional systems. Mechanizing some of these methods will reveal whether they are formally correct; performing case studies will reveal whether the methods scale and provide useful feedback. Overall, the result will be an evaluation of the published work. Should the methods turn out to be successful, then the mechanization will be useful in itself as a tool.
|
|
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 |