EPSRC logo

Details of Grant 

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 Laboratory
Organisation: University of Cambridge
Scheme: Standard Research (Pre-FEC)
Starts: 17 January 2000 Ends: 16 June 2003 Value (£): 157,756
EPSRC Research Topic Classifications:
Artificial Intelligence
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
No information has been submitted for this grant.
Potential use in non-academic contexts
No information has been submitted for this grant.
Impacts
No information has been submitted for this grant.
Sectors submitted by the Researcher
No information has been submitted for this grant.
Project URL:  
Further Information:  
Organisation Website: http://www.cam.ac.uk