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:
- to prove the existence of fixed points, and
- 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.
More information can be found at CSP-Prover's homepage.