(**
 
 << CSPProver >> 
 
 August 2004 
 January 2005 (modified) 
 February 2005 (modified) 
 June 2005 (modified) 
 July 2005 (modified) 
 November 2005 (modified) 
 April 2006 (modified) 
 September 2006 (modified) 
 August 2007 (modified) 
 February 2008 (modified) 
 July 2008 (modified) 
 July 2009 (modified) 
 January 2010 (modified) 
 October 2010 (modified) 
 April 2011 (modified) 
 November 2012 (modified) 
 June 2013 (modified) 
 May 2016 (modified) 
 April 2018 (modified) 
 
 (on Isabelle 2017) 
 
 Yoshinao Isobe (AIST JAPAN) 
 Markus Roggenbach (SU UK) 
 
**)
1. Introduction
CSPProver [1,2,3,4] is an interactive theorem prover dedicated to
refinement proofs within the process algebra CSP [5]. It aims
specifically at proofs on infinite state systems, which may also
involve infinite nondeterminism.
2. Directory
CSPProver + CSP

+ CSP_T

+ CSP_F

+ FNF_F

+ DFP


+ ep2

+ DM

+ Test

+ SA_Kung

+ NBuff

+ UCD
o CSP : the reusable part of CSPProver
o CSP_T : the instantiated part for T
o CSP_F : the instantiated part for F
o FNF_F : full normalising for F
o DFP : (Deadlock Freedom Proof) on CSP_F, theorems given in [6]
o ep2 : an example (electronic payment system) on CSP_F
o DM : an example (Dining Mathematicians) on CSP_F
o Test : small examples on CSP_F
o SA_Kung: an example on DFP (Kung's Systolic array [3])
o NBuff : an example (Linked n onebuffers)
o UCD : an example (Uniform Candy Distribution Puzzle [1])
3. Installation
This CSPProver needs Isabelle2016.
At first, the environmentvariable "CSP_PROVER_HOME" is set to
the directory containing CSP, CSP_T,..., and ROOT of CSPProver.
To make heapfiles of CSP, CSP_T, CSP_F, and FNF_F once, execute the
command "make_heap" in this directory (CSP_PROVER_HOME).
Please read "User Guide CSPProver". The latest version can be
downloaded from the CSPProver's website:
http://staff.aist.go.jp/yisobe/CSPProver/CSPProver.html
4. User interface
To start Iasbelle/jEdit with the logic of CSP_F, execute the following
command:
isabelle jedit d '$CSP_PROVER_HOME' l CSP_F
5. Licence agreement
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). The details are given in
http://staff.aist.go.jp/yisobe/CSPProver/licence.txt
You have to agree with the licence before using CSPProver.
6. Xsymbols
Xsymbols are used for expressing conventional CSP operators in
CSPProver, but Xsymbols may causes some warnings on syntax.
Therefore, we separated the definitions of Xsymbols from the main
definitions and theorems, and collected them into new files
"CSP_*_xsymbols". If you do not use Xsymbols of CSPProcesses, it is
recommended to use the theories
CSP_Main, CSP_T_Main, and CSP_F_Main,
instead of
CSP, CSP_T, and CSP_F.
CSP_*_Main contains all the definitions and theorems of previous
CSPProver except the definitions on Xsymbols, and CSP_* imports
CSP_*_Main and CSP_*_xsymbols.
References
[1] Y.Isobe and M.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.
[2] Y.Isobe and M.Roggenbach: A complete axiomatic semantics for the
CSP stablefailures model, CONCUR 2006 (17th International
Conference on Concurrency Theory), LNCS 4137, Springer,
pp.158172, August 2006.
[3] 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.
[4] Y.Isobe and M.Roggenbach: A generic theorem prover of CSP
refinement, TACAS 2005 (11th Inter\national Conference on Tools
and Algorithms for the Construction and Analysis of Systems), LNCS
3440, Springer, pp.108123, April 2005.
[5] A.W.Roscoe, "The Theory and Practice of Concurrency",
Prentice Hall, 1998.
[6] A.W.Roscoe and N.Dathi, "The pursuit of deadlock freedom",
Information and Computation, Vol.75, No.3, pp.289327, 1987.