CSP-prover swMATH ID: 11465 Software Authors: Isobe, Yoshinao; Roggenbach, Markus Description: 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. .. Homepage: https://staff.aist.go.jp/y-isobe/CSP-Prover/CSP-Prover.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 – CSP-prover in practice. Zbl 1218.68105Isobe, Yoshinao; Roggenbach, Markus 2008 A generic theorem prover of CSP refinement. Zbl 1087.68592Isobe, Yoshinao; Roggenbach, Markus 2005 all top 5 Cited by 30 Authors 7 Roggenbach, Markus 5 Isobe, Yoshinao 2 Cavalcanti, Ana 1 Baxter, James 1 Calder, Muffy 1 Chen, Zhenbang 1 Dong, JinSong 1 Falcão, Flávia 1 Foster, Simon 1 Iyoda, Juliano 1 Kahsai, Temesghen 1 Kleine, Moritz 1 Liu, Yang 1 Liu, Zhiming 1 Miller, Alice Ann 1 Murray, Toby 1 O’Reilly, Liam 1 Qin, Shengchao 1 Reeves, Steve 1 Ribeiro, Pedro 1 Sampaio, Augusto C. A. 1 Samuel, D. Gift 1 Shi, Ling 1 Steyn, T. J. 1 Streader, David 1 Sun, Jun 1 Wang, Ji 1 Woodcock, James C. P. 1 Ye, Kangfeng 1 Zhao, Yongxin all top 5 Cited in 6 Serials 2 Theoretical Computer Science 2 Formal Aspects of Computing 1 Acta Informatica 1 Information Processing Letters 1 Electronic Notes in Theoretical Computer Science 1 Journal of Logical and Algebraic Methods in Programming Cited in 2 Fields 17 Computer science (68-XX) 1 General and overarching topics; collections (00-XX) Citations by Year