HOL-CSP Version 2.0


Title: HOL-CSP Version 2.0
Authors: Safouan Taha (safouan /dot/ taha /at/ lri /dot/ fr), Lina Ye (lina /dot/ ye /at/ lri /dot/ fr) and Burkhart Wolff (wolff /at/ lri /dot/ fr)
Submission date: 2019-04-26
Abstract: This is a complete formalization of the work of Hoare and Roscoe on the denotational semantics of the Failure/Divergence Model of CSP. It follows essentially the presentation of CSP in Roscoe’s Book ”Theory and Practice of Concurrency” [8] and the semantic details in a joint Paper of Roscoe and Brooks ”An improved failures model for communicating processes". The present work is based on a prior formalization attempt, called HOL-CSP 1.0, done in 1997 by H. Tej and B. Wolff with the Isabelle proof technology available at that time. This work revealed minor, but omnipresent foundational errors in key concepts like the process invariant. The present version HOL-CSP profits from substantially improved libraries (notably HOLCF), improved automated proof techniques, and structured proof techniques in Isar and is substantially shorter but more complete.
  author  = {Safouan Taha and Lina Ye and Burkhart Wolff},
  title   = {HOL-CSP Version 2.0},
  journal = {Archive of Formal Proofs},
  month   = apr,
  year    = 2019,
  note    = {\url{http://isa-afp.org/entries/HOL-CSP.html},
            Formal proof development},
  ISSN    = {2150-914x},
License: BSD License
Status: [ok] This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.