Automating refinement of Circus programs

DOI10.1007/978-3-642-19829-8_18zbMATH Open1325.68163OpenAlexW153095480MaRDI QIDQ2999326FDOQ2999326

Authors: Frank Zeyda, Ana Cavalcanti 

Publication date: 12 May 2011

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

Full work available at URL: https://doi.org/10.1007/978-3-642-19829-8_18

Recommendations

• Encoding Circus programs in ProofPower-Z
• A refinement strategy for Circus
• A tactic language for refinement of state-rich concurrent specifications
• Testing for refinement in \textsf{Circus}
• scientific article; zbMATH DE number 2090152

zbMATH Keywords

theorem provingtacticsArcAngel CProofPower

Mathematics Subject Classification ID

Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Cites Work

• Saoithín: a theorem prover for UTP
• A tactic language for refinement of state-rich concurrent specifications
• ArcAngel: a tactic language for refinement
• A tactic calculus. --- Abridged version
• Mechanical reasoning about families of UTP theories
• FM 2005: Formal Methods
• A refinement strategy for Circus

Cited In (7)

• Mechanised support for sound refinement tactics
• FM 2005: Formal Methods
• A refinement strategy for Circus
• Encoding Circus programs in ProofPower-Z
• A tactic language for refinement of state-rich concurrent specifications
• Type checking \textsf{Circus} specifications
• Simpler reasoning about system properties: a proof-by-refinement technique

Uses Software

• ArcAngel
• ArcAngelC
• ProofPower
• Z
• Circus

This page was built for publication: Automating refinement of Circus programs

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