Mechanical Reasoning about Families of UTP Theories

DOI10.1016/J.ENTCS.2009.05.055zbMath1347.68098OpenAlexW2037100211MaRDI QIDQ5179366

Frank Zeyda, Ana Cavalcanti

Publication date: 19 March 2015

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

Full work available at URL: https://doi.org/10.1016/j.entcs.2009.05.055

zbMATH Keywords

theorem provingsemantic embedding

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (2)

UTPCalc — A Calculator for UTP Predicates ⋮ Isabelle/UTP: A Mechanised Theory Engineering Framework

Uses Software

• ProofPower
• ClawZ
• Circus

Cites Work

• A refinement strategy for Circus
• Unifying Theories in ProofPower-Z
• Pointers and Records in the Unifying Theories of Programming
• Mechanising a Unifying Theory
• Unnamed Item

This page was built for publication: Mechanical Reasoning about Families of UTP Theories