Mechanical Reasoning about Families of UTP Theories

DOI10.1016/J.ENTCS.2009.05.055zbMATH Open1347.68098OpenAlexW2037100211MaRDI QIDQ5179366FDOQ5179366

Authors: 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

Recommendations

• Mechanical reasoning about families of UTP theories
• Isabelle/UTP: a mechanised theory engineering framework
• scientific article; zbMATH DE number 1088189
• Higher-order UTP for a theory of methods
• Mechanizing coinduction and corecursion in higher-order logic
• Mechanizing proofs with logical relations -- Kripke-style
• On mechanizing proofs within a complete proof system for Unity
• scientific article; zbMATH DE number 3941499
• scientific article; zbMATH DE number 3948225

zbMATH Keywords

theorem provingsemantic embedding

Mathematics Subject Classification ID

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

Cites Work

• Title not available (Why is that?)
• Unifying Theories in ProofPower-Z
• Mechanising a Unifying Theory
• A refinement strategy for Circus
• Pointers and Records in the Unifying Theories of Programming

Cited In (9)

• The Linear Algebra of UTP
• Isabelle/UTP: A Mechanised Theory Engineering Framework
• Mechanising a Unifying Theory
• Unifying Theories in ProofPower-Z
• Mechanical reasoning about families of UTP theories
• UTPCalc — A Calculator for UTP Predicates
• Semantic inheritance in unifying theories of programming
• Unifying theories in ProofPower-Z
• Saoithín: a theorem prover for UTP

Uses Software

• ProofPower
• ClawZ
• Circus

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5179366)