Towards a model-checker for \textit{\textsf{Circus}}

DOI10.1007/978-3-030-30942-8_14zbMATH Open1539.68163MaRDI QIDQ6535951

Artur Oliveira Gomes, Andrew Butterfield

Publication date: 14 March 2024

zbMATH Keywords

Circus

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Computing maximal weak and other bisimulations
• A refinement strategy for Circus
• Test generation from state based use case models
• ZRC -- A refinement calculus for \(Z\)
• Unifying theories in ProofPower-Z
• Isabelle/UTP: A Mechanised Theory Engineering Framework
• Guarded commands, nondeterminacy and formal derivation of programs
• From LOTOS to LNT
• FDR3 — A Modern Refinement Checker for CSP
• FM 2005: Formal Methods

This page was built for publication: Towards a model-checker for \textit{\textsf{Circus}}