Technical reports
Mechanizing compositional reasoning for concurrent systems: some lessons
August 2003, 20 pages
DOI: 10.48456/tr-573
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 = {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-573.pdf}, institution = {University of Cambridge, Computer Laboratory}, doi = {10.48456/tr-573}, number = {UCAM-CL-TR-573} }