Automating refinement of Circus programs

DOI10.1007/978-3-642-19829-8_18MaRDI QIDQ2999326zbMATH OpenOpenAlexFDO

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

zbMATH Keywords

theorem provingtacticsArcAngel CProofPower

Mathematics Subject Classification ID

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

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

Cites work

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

Cited in

(7)

• Mechanised support for sound refinement tactics
• A refinement strategy for Circus
• FM 2005: Formal Methods
• 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

Describes a project that uses

Uses Software

• Circus
• Z
• ProofPower
• ArcAngelC
• ArcAngel

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)