CSPprover
swMATH ID:  11465 
Software Authors:  Isobe, Yoshinao; Roggenbach, Markus 
Description:  CSPProver 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 nondeterminism. For this reason, CSPProver currently focuses on the stable failures model F as the underlying denotational semantics of CSP. Semantically, CSPProver 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. CSPProver implements both these theories for infinite product spaces and thus is capable to deal with infinite systems of process equations. Technically, CSPProver is based on the generic theorem prover Isabelle, using the logic HOLComplex. Within this logic, the syntax as well as the semantics of CSP is encoded, i.e., CSPProver provides a deep encoding of CSP. The tool’s architecture follows a generic approach which makes it easy to reuse large parts of the encoding for other CSP models. For instance, merely as a byproduct, CSPProver includes also the CSP traces model T. More importantly, CSPProver can easily be extended to the failuredivergence model N and the various infinite traces models of CSP. .. 
Homepage:  https://staff.aist.go.jp/yisobe/CSPProver/CSPProver.html 
Related Software:  PVS; Isabelle/HOL; FDR2; Z; CASL; PAT; Circus; HOL; Isabelle; Hets; GitHub; Esterel; FDR3; ProB; Archive Formal Proofs; Isabelle/UTP; PTSC; ProofPower; TCOZ; ML 
Cited in:  17 Publications 
Standard Articles
2 Publications describing the Software, including 2 Publications in zbMATH  Year 

Proof principles of CSP – CSPprover in practice. Zbl 1218.68105 Isobe, Yoshinao; Roggenbach, Markus 
2008

A generic theorem prover of CSP refinement. Zbl 1087.68592 Isobe, Yoshinao; Roggenbach, Markus 
2005

all
top 5
Cited by 30 Authors
all
top 5
Cited in 6 Serials
Cited in 2 Fields
17  Computer science (68XX) 
1  General and overarching topics; collections (00XX) 