 (17/12/2020) The GitHub page for CSPProver is available.
 (18/04/2020) CSPProver Ver.5.1 for Isabelle 2020 was released on 18 April 2020. The definitions, lemmas, and theorems are the same as CSPProver Ver.5.1 for Isabelle 2018.
 (18/02/2019) CSPProver Ver.5.1 for Isabelle 2018 was released on 18 February 2019. The definitions, lemmas, and theorems are the same as CSPProver Ver.5.1 for Isabelle 2017.
 (09/08/2018) CSPProver Ver.5.1 for Isabelle 2017 was released on 9 August 2018. The definitions, lemmas, and theorems are the same as CSPProver Ver.5.1 for Isabelle 2016.
 (09/05/2016) CSPProver Ver.5.1 for Isabelle 2016 was released on 9 May 2016. The definitions, lemmas, and theorems are the same as CSPProver Ver.5.1 for Isabelle 2013.
 (~2015)
 Verification of infinite state systems. For example, we applied CSPProver 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, CSPProver 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 CSPProver30.tar.gz or later.
CSPProver 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 nondeterminism. For this reason,
CSPProver currently focuses on the stable failures model F
as the underlying denotational semantics of CSP.
Semantically, CSPProver 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. CSPProver implements both these theories for infinite product spaces and thus is capable to deal with infinite systems of process equations.
Technically, CSPProver is based on the generic theorem prover Isabelle, using the logic HOLComplex. Within this logic, the syntax as well as the semantics of CSP is encoded, i.e., CSPProver provides a deep encoding of CSP. The tool's architecture follows a generic approach which makes it easy to reuse large parts of the encoding for other CSP models. For instance, merely as a byproduct, CSPProver includes also the CSP traces model T. More importantly, CSPProver can easily be extended to the failuredivergence model N and the various infinite traces models of CSP.
Consequently, CSPProver contains fundamental theorems such as fixed point theorems on cpo and cms, the definitions of CSP syntax and semantics, and many CSPlaws and semiautomatic proof tactics for verification of refinement relation. Therefore, CSPProver can be used for
Semantically, CSPProver 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. CSPProver implements both these theories for infinite product spaces and thus is capable to deal with infinite systems of process equations.
Technically, CSPProver is based on the generic theorem prover Isabelle, using the logic HOLComplex. Within this logic, the syntax as well as the semantics of CSP is encoded, i.e., CSPProver provides a deep encoding of CSP. The tool's architecture follows a generic approach which makes it easy to reuse large parts of the encoding for other CSP models. For instance, merely as a byproduct, CSPProver includes also the CSP traces model T. More importantly, CSPProver can easily be extended to the failuredivergence model N and the various infinite traces models of CSP.
Consequently, CSPProver contains fundamental theorems such as fixed point theorems on cpo and cms, the definitions of CSP syntax and semantics, and many CSPlaws and semiautomatic proof tactics for verification of refinement relation. Therefore, CSPProver can be used for

Source Package:
(requires Isabelle 20091 or Isabelle 20092 or Isabelle 2011 or Isabelle 2012 or
Isabelle 2013 or Isabelle 2016 or Isabelle 2017 or Isabelle 2018 or Isabelle 2020)

Download [CSPProver512020.tar.gz]
(313KB) (18/04/2020)
for Isabelle 2020 
Download [CSPProver512018.tar.gz]
(312KB) (18/02/2019)
for Isabelle 2018 
Download [CSPProver512017.tar.gz]
(311KB) (23/04/2018)
for Isabelle 2017  [previous versions]

Download [CSPProver512020.tar.gz]
(313KB) (18/04/2020)

Unpack it, e.g. by tar zxvf CSPProver51201?.tar.gz.
CSPProver512017 contains the following 11 directories [README]:
CSP theory packages (for 2017)
 CSP ( README, theory files, dependencygraph )
 CSP_T ( README, theory files, dependencygraph )
 CSP_F ( README, theory files, dependencygraph )
 FNF_F ( README, theory files, dependencygraph )
 DFP ( README, theory files, dependencygraph )
 Examples (for 2017)

CSP theory packages (for 2017)

"User Guide CSPProver Ver.5.0":

Download [UserGuide51.pdf] (276KB)
(last modified: 06/01/2010)
You can download CSPProver:
Following the ideas of open source software, we allow anyone
to use CSPProver without fee, under
the CSPProver licence,
which is similar to the Lesser Gnu Public License
(LGPL). You have to agree with the licence before using
CSPProver.

Go to the directory CSPProver by
cd /user/local/CSPProver512017 
Execute a command by
make_heaps
Click here for CSPProver512017
It is assumed that "CSPProver512017.tar.gz" has been downloaded (see Download) and has been unpacked to the directory (or your appropriate directory):
/user/local/CSPProver512017
It is recommended that you make heap files CSP, CSP_T, CSP_F, FNF_F, and DFP by:
~/.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 CSPProver Ver.5.1" (see Download) for detail)
It is assumed that "CSPProver512017.tar.gz" has been downloaded (see Download) and has been unpacked to the directory (or your appropriate directory):
/user/local/CSPProver512017
It is recommended that you make heap files CSP, CSP_T, CSP_F, FNF_F, and DFP by:
~/.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 CSPProver 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]
 Yoshinao Isobe and Markus Roggenbach, CSPProver  a Proof Tool for the Verification of Scalable Concurrent Systems, Journal of Computer Software, Japan Society for Software Science and Technology (JSSST), Vol.25, No.4, pp.8592, 2008. [PDF: 245KB]
 Yoshinao Isobe and Markus Roggenbach, Proof Principles of CSP  CSPProver in Practice, Dynamics in Logistics: First International Conference, LDIC 2007, Springer, pp.425422, 2007.
 Yoshinao Isobe and Markus Roggenbach, A complete axiomatic semantics for the CSP stablefailures model, CONCUR 2006 (17th International Conference on Concurrency Theory), LNCS 4137, Springer, pp.158172, Bonn (Germany), August 2006. [PDF: 210KB]
 Y.Isobe, M.Roggenbach, and S.Gruner, Extending CSPProver by deadlockanalysis: Towards the verification of systolic arrays, FOSE 2005 (12th Workshop on Foundation of Software Engineering), Japanese Lecture Notes Series 31, pp.257266, Kindaikagakusha, November 2005.
 Y.Isobe and M.Roggenbach, A generic theorem prover of CSP refinement, TACAS 2005 (11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems), LNCS 3440, Springer, pp.108123, Edinburgh (U.K.), April 2005. [PDF: 254KB]
 Y.Isobe and M.Roggenbach: CSPProver, a Theorem Prover for a Process Algebra CSP (in Japanese), PRO 52th meeting, IPSJ (Information Processing Society of Japan), January 2005. [PDF: 233KB]
FACCS Workshop "25 years of CSP", Southbank University London, 7 and 8
July, 2004
We would like to thank
Christoph Lüth,
Ranko Lazic,
BerndHolger Schlingloff, and
Jan Peleska
for valuable feedback and advice to improve our tool.

Yoshinao Isobe
Cyber Physical Security Research Center
National Institute of Advanced Industrial Science and Technology (AIST)
email: yisobe@aist.go.jp 
Markus Roggenbach
Department of Computer Science
College of Science
Swansea University
email: M.Roggenbach@swan.ac.uk