Unifying theories in ProofPower-Z

DOI10.1007/S00165-007-0044-5zbMath1259.68035OpenAlexW2006972847MaRDI QIDQ1941892

Ana Cavalcanti, J. C. P. Woodcock, Marcel V. M. Oliveira

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

theorem provingrelational semanticsCircus

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (6)

Unifying Theories of Programming in Isabelle ⋮ Theoretical and practical approaches to the denotational semantics for MDESL based on UTP ⋮ Denotational semantics and its algebraic derivation for an event-driven system-level language ⋮ An Axiomatic Value Model for Isabelle/UTP ⋮ Modelling temporal behaviour in complex systems with Timebands ⋮ Simulink Timed Models for Program Verification

Uses Software

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

Cites Work

• A refinement strategy for Circus
• Angelic nondeterminism in the unifying theories of programming
• Edinburgh LCF. A mechanized logic of computation
• Unifying Theories in ProofPower-Z
• Mechanising a Unifying Theory
• FM 2005: Formal Methods
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

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