Automating Refinement of Circus Programs

DOI10.1007/978-3-642-19829-8_18zbMath1325.68163OpenAlexW153095480MaRDI QIDQ2999326

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)

Related Items (1)

Mechanised support for sound refinement tactics

Uses Software

• ArcAngel
• ArcAngelC
• ProofPower
• Z
• Circus

Cites Work

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

This page was built for publication: Automating Refinement of Circus Programs