Technical reports

Mechanizing UNITY in Isabelle

Lawrence C. Paulson

June 1999, 22 pages

DOI: 10.48456/tr-467

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 = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-467.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-467},
  number = 	 {UCAM-CL-TR-467}
}