Unifying theories in ProofPower-Z

DOI10.1007/S00165-007-0044-5MaRDI QIDQ1941892zbMATH OpenOpenAlexFDO

Authors Ana Cavalcanti, Marcel V. M. Oliveira, Jim Woodcock

Publication date 22 March 2013

Published in Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s00165-007-0044-5

zbMATH Keywords

relational semanticstheorem provingCircus

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

• Unifying Theories in ProofPower-Z
• Mechanical reasoning about families of UTP theories
• Mechanising a Unifying Theory
• Mechanical Reasoning about Families of UTP Theories
• Unifying theories of programming in Isabelle

Cites work

• 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 605806 (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?)
• scientific article; zbMATH DE number 1487746 (Why is no real title available?)
• scientific article; zbMATH DE number 234014 (Why is no real title available?)
• scientific article; zbMATH DE number 958048 (Why is no real title available?)
• A refinement strategy for Circus
• Angelic nondeterminism in the unifying theories of programming
• Edinburgh LCF. A mechanized logic of computation
• FM 2005: Formal Methods
• Mechanising a Unifying Theory
• Unifying Theories in ProofPower-Z

Cited in

(13)

• Mechanical reasoning about families of UTP theories
• Mechanising a Unifying Theory
• Unifying Theories in ProofPower-Z
• Modelling temporal behaviour in complex systems with Timebands
• Simulink timed models for program verification
• Denotational semantics and its algebraic derivation for an event-driven system-level language
• An Axiomatic Value Model for Isabelle/UTP
• Theoretical and practical approaches to the denotational semantics for MDESL based on UTP
• A stepwise approach to linking theories
• Encoding Circus programs in ProofPower-Z
• Unifying theories of programming in Isabelle
• UTP, \textsf{\textit{Circus}}, and Isabelle
• Towards a model-checker for \textit{\textsf{Circus}}

Describes a project that uses

Uses Software

• Circus
• Z
• Z/EVES
• ProofPower
• HOL
• ML

This page was built for publication: Unifying theories in ProofPower-Z

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