AIST and Swansea University
last updated 2023.08.03
[ Isobe > CSP-Prover ]
  • (17/12/2020) The GitHub page for CSP-Prover is available.
  • (18/04/2020) CSP-Prover Ver.5.1 for Isabelle 2020 was released on 18 April 2020. The definitions, lemmas, and theorems are the same as CSP-Prover Ver.5.1 for Isabelle 2018.
  • (18/02/2019) CSP-Prover Ver.5.1 for Isabelle 2018 was released on 18 February 2019. The definitions, lemmas, and theorems are the same as CSP-Prover Ver.5.1 for Isabelle 2017.
  • (09/08/2018) CSP-Prover Ver.5.1 for Isabelle 2017 was released on 9 August 2018. The definitions, lemmas, and theorems are the same as CSP-Prover Ver.5.1 for Isabelle 2016.
  • (09/05/2016) 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 2013.
  • (~2015)

    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.

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-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):


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

a screen-shot


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


    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)

  • Yoshinao Isobe
    Cyber Physical Security Research Center
    National Institute of Advanced Industrial Science and Technology (AIST)
    e-mail: y-isobe@aist.go.jp
  • Markus Roggenbach
    Department of Computer Science
    College of Science
    Swansea University
    e-mail: M.Roggenbach@swan.ac.uk
counter (since 28/01/2005)