Computer Laboratory

Technical reports

Mechanizing UNITY in Isabelle

Lawrence C. Paulson

June 1999, 22 pages

Abstract

UNITY is an abstract formalism for proving properties of concurrent systems, which typically are expressed using guarded assignments [Chandy and Misra 1988]. UNITY has been mechanized in higher-order logic using Isabelle, a proof assistant. Safety and progress primitives, their weak forms (for the substitution axiom) and the program composition operator (union) have been formalized. To give a feel for the concrete syntax, the paper presents a few extracts from the Isabelle definitions and proofs. It discusses a small example, two-process mutual exclusion. A mechanical theory of unions of programs supports a degree of compositional reasoning. Original work on extending program states is presented and then illustrated through a simple example involving an array of processes.

Full text

PDF (0.3 MB)

BibTeX record

@TechReport{UCAM-CL-TR-467,
  author =	 {Paulson, Lawrence C.},
  title = 	 {{Mechanizing UNITY in Isabelle}},
  year = 	 1999,
  month = 	 jun,
  url = 	 {http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-467.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  number = 	 {UCAM-CL-TR-467}
}