Mechanised support for sound refinement tactics

DOI10.1007/s00165-011-0218-zzbMath1242.68077OpenAlexW2064074798MaRDI QIDQ432151

Ana Cavalcanti, Frank Zeyda, Marcel V. M. Oliveira

Publication date: 3 July 2012

Published in: Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00165-011-0218-z

zbMATH Keywords

Zrefinementautomationunifying theoriestactic language

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (2)

Safety-critical Java programs from \textsf{Circus} models ⋮ Laws of mission-based programming

Uses Software

• ML
• ArcAngel
• ArcAngelC
• ProofPower
• ClawZ
• Z
• ZRC
• Circus

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Mechanical reasoning about families of UTP theories
• A tactic language for refinement of state-rich concurrent specifications
• ArcAngel: a tactic language for refinement
• Angelic nondeterminism in the unifying theories of programming
• A UTP semantics for \textsf{Circus}
• A program refinement tool
• ZRC -- A refinement calculus for \(Z\)
• A tactic calculus. --- Abridged version
• Automating Refinement of Circus Programs
• Patterns for Refinement Automation
• Encoding Circus Programs in ProofPowerZ
• The B-Book
• The specification statement
• Unifying Theories in ProofPower-Z
• On the calculus of relations

This page was built for publication: Mechanised support for sound refinement tactics