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

semantic embeddingtheorem proving

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

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

Cited in

(10)

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

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)