an interactive theorem
prover on the process algebra CSP based on the
theorem prover Isabelle

News

- (09/05/2016) (new) CSP-Prover
Ver.5.1 for Isabelle 2016 was
released on 9 May 2016. The definitions, lemmas, and theorems are the same as CSP-Prover
Ver.5.1 for Isabelle 2016.

- (11/06/2013) CSP-Prover
Ver.5.1 for Isabelle 2013 was
released on 6 June 2013. The definitions, lemmas, and theorems are the same as CSP-Prover
Ver.5.1 for Isabelle 2013.

- (17/11/2012) CSP-Prover
Ver.5.1 for Isabelle 2012 was
released on 17 November 2012. The definitions, lemmas, and theorems are the same as CSP-Prover
Ver.5.1 for Isabelle 2011.

- (02/04/2011) CSP-Prover
Ver.5.1 for Isabelle 2011 was
released on 2 April 2011. The definitions, lemmas, and theorems are the same as CSP-Prover
Ver.5.1 for Isabelle 2009-2.

- (26/10/2010) CSP-Prover
Ver.5.1 for Isabelle 2009-2 was
released on 26 October 2010. The definitions, lemmas, and theorems are the same as CSP-Prover
Ver.5.1 for Isabelle 2009-1, but some notations were changed in accordance with Isabelle 2009-2 syntax. For example, "axclass" was replaced by "class" for declaring classes like cpo and cms.

- (06/01/2010) CSP-Prover
Ver.5.1 for Isabelle 2009-1 was
released on 6 January 2010. The definitions, lemmas, and theorems are the same as Ver.5.0 except that:

- Convenient 3 notations (<--, <<-, <==) for renaming are defined and auxiliary laws for them are proven. See the last paragraph in Section 7.1 of the User-Guide-5-1.
- The
concatenation operator of traces "^^" is replaced by "^^^" for avoiding
ambiguity because "^^" is used as the power function's symbol in Isabelle 2009-1.

- (23/07/2009) CSP-Prover
Ver.5.0 for Isabelle 2009 was
released on 23 July 2009. The main differences from version 4 are summarized as follows:

- The CSP semi-automatic proof commands are implemented as Isabelle-methods instead of ML-functions. See the last paragraph in Section 8.3 of the User-Guide-5-0.
- Convenient
2 notations (<-->, <==>) for renaming are introduced and
auxiliary laws for them are added to CSP-proof commands. See the last paragraph in Section 7.1 of the User-Guide-5-0.

- (03/11/2008) Uniform Candy
Distribution Puzzle (test version) for Isabelle 2008 was published
on 03 November 2008.

- (30/06/2008) CSP-Prover
Ver.4.0 for Isabelle 2008 was released on 30 June 2008.

- CSP-Prover Ver.4.0 is now available for Isabelle 2005, 2007, and 2008. See here.
- In this version, the definitions on X-symbols of CSP-processes
are separated from main theory files for avoiding a lot of warnings.
(see here)

- (18/02/2008) CSP-Prover
Ver.4.0 for Isabelle 2007 was released on 18 February 2008.

- CSP-Prover Ver.4.0 is now available for both Isabelle 2005 and
Isabelle 2007. See here.

- This version for Isabelle 2007 unexpectedly causes warnings
such that Currently parsed expression could be extremely ambiguous,
which does not happen in Isabelle 2005. We are now looking for the
cause.

- (22/01/2008) A test version of the developing
CSP-Prover
Ver.4.1 and
a case study by Uniform Candy Distribution Puzzle were published on
22 January 2008.

- (28/08/2007) CSP-Prover
Ver.4.0 was
released on 28 August 2007.

- The most important difference from the
previous version
(CSP-Prover-3-0) is that process names are explicitly introduced in the
basic syntax of the version 4.0.
We theoretically studied how recursions can be expressed by replicated
internal choices instead of process names in CSP-Prover-3.0, and then
we got some interesting results. However, we found that it would
be better to use process names for expressing recursions more
naturally. Process names were introduced also in
old versions (e.g CSP-Prover2005), but they are expressed in a more
elegant style in the version 4.

- (04/04/2007) A
development
snapshot (Ver.4.00) of
the next
version of CSP-Prover was published on 4 April
2007.

- (10/05/2006) CSP-Prover
Ver.3.0, which includes theorems
for a complete axiom system, was
released on 10 May 2006. The differences from previous version
(CSP-Prover2005-2) are summarized as follows:

- New CSP-laws were added, and the completeness of CSP-laws was proven in a new package FNF_F.
- The power of Replicated internal choice was extended. It
allowed our CSP dialect to be expressive with respect to the
stable-failures domain.

- Single recursive operator MU, (replicated) alphabetized
parallel operator, depth-restriction operator were added.

- All the theory files were polished and reorganized to packages CSP, CSP_T, and CSP_F.
- The expressions of recursive processes were improved in more
elegant style.

- etc

- (07/11/2005) A development
snapshot (Ver.3.01) of
the next
version of CSP-Prover was published on 7 November
2005.

- (06/07/2005) A
development snapshot of the next
version of CSP-Prover with a DFP package was published on 6 July
2005.

- (13/02/2005) A new version "CSP-Prover2005-2" was released on 13 February 2005.

[history]

Introduction

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.

Download (CSP-Prover ver.5.1)

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)

- Download [CSP-Prover-5-1-2016.tar.gz]
(293KB)
(09/05/2016--) (new)

for Isabelle 2016 - Download [CSP-Prover-5-1-2013.tar.gz]
(293KB)
(11/06/2013--)

for Isabelle 2013

- Download [CSP-Prover-5-1-2012.tar.gz]
(293KB)
(17/11/2012--)

for Isabelle 2012

- Download [CSP-Prover-5-1-2011.tar.gz]
(289KB)
(02/02/2011--)

for Isabelle 2011

- Download [CSP-Prover-5-1-2009-2.tar.gz]
(288KB)
(26/10/2010--)

for Isabelle 2009-2

- Download [CSP-Prover-5-1-2009-1.tar.gz]
(287KB)
(06/01/2010--)

for Isabelle 2009-1

Unpack it, e.g. by tar zxvf CSP-Prover-5-1-2009-1.tar.gz.

CSP-Prover-5-1-2009-1 contains the following 11 directories [README]:

CSP theory packages (for 2009-1)

œ 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 2009-1)

œ

Test

(README)

œ

ep2

(README) œ

DM

(README) œ

SA_Kung

(README) œ

NBuff

(README) œ

UCD

(README)

- "User Guide CSP-Prover Ver.5.0":

Licence agreement

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.

Set up CSP-Prover

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

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

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

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

- Go to the directory CSP-Prover by

cd /user/local/CSP-Prover-5-1-2009-1

- Execute a command by

make_heaps

~/.isabelle/heaps/Isabelle2009/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)

Example

- 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]

Papers

- Yoshinao Isobe and Markus Roggenbach: CSP-Prover -- 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.85--92, 2008.
- Yoshinao Isobe
and Markus Roggenbach, Proof Principles of CSP -- CSP-Prover in
Practice, Dynamics in Logistics: First International Conference, LDIC 2007, Springer, pp.425-422, 2007.
- Yoshinao Isobe and Markus Roggenbach: A complete axiomatic
semantics for the
CSP stable-failures model, CONCUR 2006 (17th International Conference on
Concurrency Theory), LNCS
**4137**, Springer, pp.158-172, Bonn (Germany), August 2006.

- Y.Isobe, M.Roggenbach, and S.Gruner, Extending CSP-Prover by
deadlock-analysis: Towards the verification of systolic arrays, FOSE 2005 (12th Workshop on Foundation of
Software Engineering), Japanese
Lecture Notes Series 31, pp.257-266, Kindai-kagaku-sha, November
2005.

- 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.108-123, Edinburgh (U.K.), April 2005. [pdf]

- Y.Isobe and M.Roggenbach: CSP-Prover:
a Theorem Prover for a Process Algebra CSP (in Japanese), PRO 52th meeting, IPSJ (Information Processing Society of
Japan), January 2005. [pdf]

Tool demonstration

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

Acknowledgments

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.

Support

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

Links

- theorem prover
- process algebras on theorem provers
- etc

Contact

- Yoshinao Isobe

Information Technology Research Institute

National Institute of Advanced Industrial Science and Technology (AIST)

Tsukuba Central 2, 1-1-1, Umezono, Tsukuba, Ibaraki, 305-8568, Japan

e-mail: y-isobe@aist.go.jp

- Markus Roggenbach

Department of Computer Science

College of Science

Swansea University

Singleton Park, Swansea SA2 8PP, United Kingdom

e-mail: M.Roggenbach@swan.ac.uk

Last modified: 8 May 2016

(since 28/01/2005)