Mechanical Reasoning about Families of UTP Theories

DOI10.1016/J.ENTCS.2009.05.055MaRDI QIDQ5179366zbMATH OpenOpenAlexFDO

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

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)

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

Cites work

• scientific article; zbMATH DE number 1949640 (Why is no real title available?)
• A refinement strategy for Circus
• Mechanising a Unifying Theory
• Pointers and Records in the Unifying Theories of Programming
• Unifying Theories in ProofPower-Z

Cited in

(10)

• The Linear Algebra of UTP
• Unifying theories in ProofPower-Z
• Mechanical reasoning about families of UTP theories
• Saoithín: a theorem prover for UTP
• Isabelle/UTP: a mechanised theory engineering framework
• Mechanising a Unifying Theory
• Unifying Theories in ProofPower-Z
• UTPCalc -- a calculator for UTP predicates
• Semantic inheritance in unifying theories of programming
• The logic of \(U\cdot(TP)^{2}\)

Describes a project that uses

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)