Publication announcement:

Mechanizing compositional reasoning for concurrent systems: some
lessons

Lawrence C. Paulson

Technical report UCAM-CL-TR-573, University of Cambridge,
Computer Laboratory, August 2003, 20 pages.

This document is now available at

http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-573.pdf

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.

--
University of Cambridge, Computer Laboratory,
Technical Reports (ISSN 1476-2986)
http://www.cl.cam.ac.uk/TechReports/