Mechanical reasoning about families of UTP theories

DOI10.1016/J.SCICO.2010.02.010zbMath1243.68270OpenAlexW2049339773MaRDI QIDQ436368

Ana Cavalcanti, Frank Zeyda

Publication date: 20 July 2012

Published in: Science of Computer Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.scico.2010.02.010

zbMATH Keywords

verificationtheorem provingZCircusproofpowersemantic embedding

Mathematics Subject Classification ID

Theory of programming languages (68N15) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (6)

Higher-Order UTP for a Theory of Methods ⋮ Mechanised support for sound refinement tactics ⋮ Mechanical reasoning about families of UTP theories ⋮ An Axiomatic Value Model for Isabelle/UTP ⋮ Automating Refinement of Circus Programs ⋮ Test-data generation for control coverage by proof

Uses Software

• ProofPower
• Z
• Circus
• Unnamed Item

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Mechanical reasoning about families of UTP theories
• A refinement strategy for Circus
• A UTP semantics for \textsf{Circus}
• Type Checking Specifications
• Mechanising a Unifying Theory
• A Theory of Pointers for the UTP
• FM 2005: Formal Methods
• On the calculus of relations

This page was built for publication: Mechanical reasoning about families of UTP theories