Computer Laboratory

Technical reports

A formalization of the process algebra CCS in high order logic

Monica Nesi

42 pages

Abstract

This paper describes a mechanization in higher order logic of the theory for a subset of Milner’s CCS. The aim is to build a sound and effective tool to support verification and reasoning about process algebra specifications. To achieve this goal, the formal theory for pure CCS (no value passing) is defined in the interactive theorem prover HOL, and a set of proof tools, based on the algebraic presentation of CCS, is provided.

Full text

PDF (2.1 MB)

BibTeX record

@TechReport{UCAM-CL-TR-278,
  author =	 {Nesi, Monica},
  title = 	 {{A formalization of the process algebra CCS in high order
         	   logic}},
  url = 	 {http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-278.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  number = 	 {UCAM-CL-TR-278}
}