Computer Laboratory

Technical reports

Mechanizing compositional reasoning for concurrent systems: some lessons

Lawrence C. Paulson

August 2003, 20 pages

Abstract

The paper reports on experiences of mechanizing various proposals for compositional reasoning in concurrent systems. The work uses the UNITY formalism and the Isabelle proof tool. The proposals investigated include existential/universal properties, guarantees properties and progress sets. The paper mentions some alternative proposals that are also worth of investigation. The conclusions are that many of these methods work and are suitable candidates for further development.

Full text

PDF (0.3 MB)

BibTeX record

@TechReport{UCAM-CL-TR-573,
  author =	 {Paulson, Lawrence C.},
  title = 	 {{Mechanizing compositional reasoning for concurrent
         	   systems: some lessons}},
  year = 	 2003,
  month = 	 aug,
  url = 	 {http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-573.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  number = 	 {UCAM-CL-TR-573}
}