\textit{\textsf{Circus2CSP}}: a tool for model-checking \textit{\textsf{Circus}} using FDR

DOI10.1007/978-3-030-30942-8_15zbMATH Open1539.68164MaRDI QIDQ6535952

Andrew Butterfield, Artur Oliveira Gomes

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

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Computing maximal weak and other bisimulations
• Test generation from state based use case models
• Specification of communicating processes: temporal logic versus refusals-based refinement
• ZRC -- A refinement calculus for \(Z\)
• Guarded commands, nondeterminacy and formal derivation of programs
• FDR3 — A Modern Refinement Checker for CSP
• FM 2005: Formal Methods

This page was built for publication: \textit{\textsf{Circus2CSP}}: a tool for model-checking \textit{\textsf{Circus}} using FDR

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