A development snapshot (3.01) of CSP-Prover 3.0

(to CSP-Prover's homepage)

Introduction

We are developing the next version of CSP-Prover. The main differences from the previous version (CSP-Prover-3.00) are summarized as follows:
  1. all theory files were improved and reorganized to CSP, CSP_T, and CSP_F,
  2. simple recursion operator (MU) was added,
  3. full abstraction in F was proven by using replicated internal choice instead of general internal choice,
  4. Isabelle 2005 was used.
DFP package and the theory files for the systolic array given in CSP-Prover-3.00 are now being modified and will be added to this version soon.

Download

You can download a development snapshot of the next version of CSP-Prover:              download [CSP-Prover-3.01.tar.gz] (153KB) (07/11/2005--)


Test CSP-Prover-3.01

This version is a development snapshot of ver.3.0, but it has almost been stable. You can test to prove that ep2 is deadlock free by CSP-Prover as follows:

It is assumed that "CSP-Prover-3.01" has been downloaded and has been unpacked (e.g. tar zxvf CSP-Prover-3.01.tar.gz) to the directory (or
your appropriate directory:

   ~/tool/CSP-Prover-3.01

The directory CSP-Prover-3.01 has the tree shown in the following Figure:

     CSP-Prover-3.00 ---+--- CSP   (README, theory map)
                        |
                        +--- CSP_T (README, theory map)
                        |
                        +--- CSP_F (README, theory map)
                        |
                        +--- ep2   (README)
                        |
                        +--- DM    (README)
                        |
                        +--- Test  (README)

To prove the deadlock freedom of ep2, heap files of CSP, CSP_T, and CSP_F should be built as follows
(it requires Isabelle(2005)/HOL-Complex):
  1. make a heap files of CSP, CSP_T, and CSP_F by

       isatool usedir -b HOL-Complex CSP     (at ~/tool/CSP-Prover-3.00/CSP)
       isatool usedir -b CSP CSP_T           (at ~/tool/CSP-Prover-3.00/CSP_T)
       isatool usedir -b CSP_T CSP_F         (at ~/tool/CSP-Prover-3.00/CSP_F)

  2. Execute ProofGeneral (2005) with CSP_F as follows:

      Isabelle -l CSP_F

    at ~/tool/CSP-Prover-3.01/ep2

  3. Load the theory file "ep2_nucleus.thy" by C-x C-f.

  4. Prove the theorem by C-c C-n until the bottom.
    (or Finish the proof by C-c C-b at one step)
If you cannot use ProofGeneral, then you can also start isabelle with CSP_F as follows:

       isabelle -I CSP_F

at ~/tool/CSP-Prover-3.01/ep2 in a shell window. Then, cut and past commands from ep2_nucleus.thy to the shell window step by step.

Last modified: 07 November 2005
(since 07/11/2005)