CSP-Prover

CSP-Prover is an interactive theorem prover dedicated to refinement proofs within the process algebra CSP. It aims specifically at proofs on infinite state systems, which may also involve infinite non-determinism. For this reason, CSP-Prover currently focuses on the stable failures model F as the underlying denotational semantics of CSP.

Semantically, CSP-Prover offers both classical approaches to denotational semantics: the theory of complete partial orders (cpo) as well as the theory of complete metric spaces (cms). In this context the respective Fixed Point Theorems are used for two purposes: (1) to prove the existence of fixed points, and (2) to prove CSP refinement between two fixed points. CSP-Prover implements both these theories for infinite product spaces and thus is capable to deal with infinite systems of process equations.

Technically, CSP-Prover is based on the generic theorem prover Isabelle, using the logic HOL-Complex. Within this logic, the syntax as well as the semantics of CSP is encoded, i.e., CSP-Prover provides a deep encoding of CSP. The tool's architecture follows a generic approach which makes it easy to re-use large parts of the encoding for other CSP models. For instance, merely as a by-product, CSP-Prover includes also the CSP traces model T. More importantly, CSP-Prover can easily be extended to the failure-divergence model N and the various infinite traces models of CSP.

Consequently, CSP-Prover contains fundamental theorems such as fixed point theorems on cpo and cms, the definitions of CSP syntax and semantics, and many CSP-laws and semi-automatic proof tactics for verification of refinement relation. Therefore, CSP-Prover can be used for

• Verification of infinite state systems. For example, we applied CSP-Prover to verify a part of the specification of the ep2 system, which is a new industrial standard of electronic payment systems, explained here.
• Establishing new theorems on CSP. For example, CSP-Prover assisted us very well in proving new theorems on a sound and complete axiom system for the stable failures equivalence over processes with unbounded nondeterminism over arbitrary alphabet. The result is included in the package FNF_F, in CSP-Prover-3-0.tar.gz or later.

You can download CSP-Prover:

• Source Package: (requires Isabelle 2009-1 or Isabelle 2009-2 or Isabelle 2011 or Isabelle 2012 or Isabelle 2013 or Isabelle 2016 or Isabelle 2017 or Isabelle 2018 or Isabelle 2020)
  • Download [CSP-Prover-5-1-2020.tar.gz] (313KB) (18/04/2020--)
    for Isabelle 2020
  • Download [CSP-Prover-5-1-2018.tar.gz] (312KB) (18/02/2019--)
    for Isabelle 2018
  • Download [CSP-Prover-5-1-2017.tar.gz] (311KB) (23/04/2018--)
    for Isabelle 2017
  • [previous versions]
• Unpack it, e.g. by tar zxvf CSP-Prover-5-1-201?.tar.gz.
  CSP-Prover-5-1-2017 contains the following 11 directories [README]:
  • CSP theory packages (for 2017)
    • CSP ( README, theory files, dependency-graph )
    • CSP_T ( README, theory files, dependency-graph )
    • CSP_F ( README, theory files, dependency-graph )
    • FNF_F ( README, theory files, dependency-graph )
    • DFP ( README, theory files, dependency-graph )
  • Examples (for 2017)
    • Test ( README )
    • ep2 ( README )
    • DM ( README )
    • SA_Kung ( README )
    • NBuff ( README )
    • UCD ( README )
• "User Guide CSP-Prover Ver.5.0":
  Download [User-Guide-5-1.pdf] (276KB) (last modified: 06/01/2010)

Following the ideas of open source software, we allow anyone to use CSP-Prover without fee, under the CSP-Prover licence, which is similar to the Lesser Gnu Public License (LGPL). You have to agree with the licence before using CSP-Prover.

Click here for CSP-Prover-5-1-2017

It is assumed that "CSP-Prover-5-1-2017.tar.gz" has been downloaded (see Download) and has been unpacked to the directory (or your appropriate directory):

   /user/local/CSP-Prover-5-1-2017

It is recommended that you make heap files CSP, CSP_T, CSP_F, FNF_F, and DFP by:

1. Go to the directory CSP-Prover by
      cd /user/local/CSP-Prover-5-1-2017
2. Execute a command by
      make_heaps

The heap files will be made in your isabelle directory. If you did not specify the directory, it is probably

   ~/.isabelle/heaps/Isabelle2017/polyml-*** (which depends on your OS)

It may take time to make the heap files. For example, 8 minutes by Intel CPU (Core2, 2.5GHz).

(Please read "User Guide CSP-Prover Ver.5.1" (see Download) for detail)

The ep2 system : a new Industrial standard of electronic payment systems
--> [click here for detail]

The dining Mathematicians : a classical mutual exclusion problem
--> [click here for detail]

Uniform Candy Distribution Puzzle
--> [click here for detail]

FACCS Workshop "25 years of CSP", Southbank University London, 7 and 8 July, 2004

We would like to thank Christoph Lüth, Ranko Lazic, Bernd-Holger Schlingloff, and Jan Peleska for valuable feedback and advice to improve our tool.

This joint project between AIST (Japan) and SU (UK) is supported by the Royal Society Grants (Ref: NC/SV/Japan/isobe 15418 and an international outgoing short visit)