A generic theorem prover of CSP refinement

DOI10.1007/978-3-540-31980-1_8MaRDI QIDQ5703799zbMATH OpenOpenAlexFDO

Authors Yoshinao Isobe, Markus Roggenbach

Publication date 10 November 2005

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/b107194

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• CSP-CASL-Prover: a generic tool for process and data refinement
• Proof principles of CSP -- CSP-prover in practice
• Symbolic analysis tools for CSP
• A Complete Axiomatic Semantics for the CSP Stable-Failures Model
• scientific article; zbMATH DE number 3903944

Cited in

(14)

• A UTP semantics for communicating processes with shared variables and its formal encoding in PVS
• On the limits of refinement-testing for model-checking CSP
• Sound reasoning in \textit{tock}-CSP
• CSP-prover
• CSP-CASL -- a new integration of process algebra and algebraic specification
• Generic tools via general refinement
• Simulating truly concurrent CSP
• CSymLean: A Theorem Prover for the Logic CSL over Symmetric Minspaces
• Property Preserving Refinement for Csp-Casl
• CSP-CASL-Prover: a generic tool for process and data refinement
• The stable revivals model in CSP-Prover
• Multiple synchrony in MSC
• Proof principles of CSP -- CSP-prover in practice
• Failure-divergence semantics and refinement of long running transactions

Describes a project that uses

Uses Software

• FDR2
• PVS
• Isabelle/HOL
• HOL

This page was built for publication: A generic theorem prover of CSP refinement

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5703799)