Unifying Theories in ProofPower-Z

DOI10.1007/11768173_8zbMath1186.68090OpenAlexW2159877500MaRDI QIDQ5307478

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

Publication date: 14 September 2007

Published in: Unifying Theories of Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/11768173_8

zbMATH Keywords

theorem proverunifying theories of programming

Mathematics Subject Classification ID

General topics in the theory of software (68N01)

Related Items

Theorem proving graph grammars with attributes and negative application conditions ⋮ The Logic of U ·(TP)2 ⋮ Higher-Order UTP for a Theory of Methods ⋮ Unifying Heterogeneous State-Spaces with Lenses ⋮ TPS: A hybrid automatic-interactive system for developing proofs ⋮ Unifying theories in ProofPower-Z ⋮ Mechanised support for sound refinement tactics ⋮ Refinement-oriented models of Stateflow charts ⋮ Mechanical Reasoning about Families of UTP Theories ⋮ A UTP semantics for communicating processes with shared variables and its formal encoding in PVS ⋮ Isabelle/UTP: A Mechanised Theory Engineering Framework ⋮ A UTP semantics for \textsf{Circus} ⋮ Compositional Assume-Guarantee Reasoning of Control Law Diagrams Using UTP

Uses Software

• ProofPower