Mechanical reasoning about families of UTP theories

DOI10.1016/J.SCICO.2010.02.010MaRDI QIDQ436368zbMATH OpenOpenAlexFDO

Authors Frank Zeyda, Ana Cavalcanti

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)

Recommendations

• Mechanical Reasoning about Families of UTP Theories
• Isabelle/UTP: a mechanised theory engineering framework
• Unifying theories in ProofPower-Z
• Mechanising a Unifying Theory
• An Axiomatic Value Model for Isabelle/UTP

Cites work

• scientific article; zbMATH DE number 3821130 (Why is no real title available?)
• scientific article; zbMATH DE number 4039251 (Why is no real title available?)
• scientific article; zbMATH DE number 3574936 (Why is no real title available?)
• scientific article; zbMATH DE number 605917 (Why is no real title available?)
• scientific article; zbMATH DE number 1949640 (Why is no real title available?)
• A Theory of Pointers for the UTP
• A UTP semantics for \textsf{Circus}
• A refinement strategy for Circus
• FM 2005: Formal Methods
• Mechanical reasoning about families of UTP theories
• Mechanising a Unifying Theory
• On the calculus of relations
• Type checking \textsf{Circus} specifications

Cited in

(23)

• The Linear Algebra of UTP
• An Axiomatic Value Model for Isabelle/UTP
• Unifying theories of programming in Isabelle
• Unifying theories in ProofPower-Z
• Mechanical Reasoning about Families of UTP Theories
• Mechanised support for sound refinement tactics
• Mechanical reasoning about families of UTP theories
• Saoithín: a theorem prover for UTP
• Isabelle/UTP: a mechanised theory engineering framework
• Unifying theories of undefinedness in UTP
• Test-data generation for control coverage by proof
• A Relational Investigation of UTP Designs and Prescriptions
• Mechanising a Unifying Theory
• Unifying Theories in ProofPower-Z
• UTPCalc -- a calculator for UTP predicates
• Unifying theories in Isabelle/HOL
• Unifying theories of locations
• Higher-order UTP for a theory of methods
• Semantic inheritance in unifying theories of programming
• Unifying heterogeneous state-spaces with lenses
• The logic of \(U\cdot(TP)^{2}\)
• Unifying theories of confidentiality
• Automating refinement of Circus programs

Describes a project that uses

Uses Software

• Coq
• ProofPower
• Z
• 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 Q436368)