Technical reports
A formalization of the process algebra CCS in high order logic
Monica Nesi
42 pages
DOI: 10.48456/tr-278
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 = {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-278.pdf}, institution = {University of Cambridge, Computer Laboratory}, doi = {10.48456/tr-278}, number = {UCAM-CL-TR-278} }