Unifying theories in ProofPower-Z
DOI10.1007/S00165-007-0044-5zbMATH Open1259.68035OpenAlexW2006972847MaRDI QIDQ1941892FDOQ1941892
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
Recommendations
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?)
- Edinburgh LCF. A mechanized logic of computation
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Angelic nondeterminism in the unifying theories of programming
- Title not available (Why is that?)
- Unifying Theories in ProofPower-Z
- Mechanising a Unifying Theory
- Title not available (Why is that?)
- FM 2005: Formal Methods
- A refinement strategy for Circus
- Title not available (Why is that?)
Cited In (13)
- Mechanising a Unifying Theory
- Unifying Theories in ProofPower-Z
- Mechanical reasoning about families of UTP theories
- Modelling temporal behaviour in complex systems with Timebands
- Simulink timed models for program verification
- An Axiomatic Value Model for Isabelle/UTP
- Denotational semantics and its algebraic derivation for an event-driven system-level language
- 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}}
Uses Software
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)
