Unifying theories in ProofPower-Z

DOI10.1007/s00165-007-0044-5zbMath1259.68035MaRDI 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 proving; relational semantics; Circus

Mathematics Subject Classification ID

68Q60: Specification and verification (program logics, model checking, etc.)

68N30: Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)

Related Items

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, Modelling temporal behaviour in complex systems with Timebands, Simulink Timed Models for Program Verification, Unifying Theories of Programming in Isabelle, An Axiomatic Value Model for Isabelle/UTP

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