An Isabelle-based proof environment for UTP
Isabelle/UTP is an embedding of Hoare and He's Unifying Theories of Programming in Isabelle/HOL. The UTP is a semantic framework for the formalisation, comparison, and integration of a variety of a computational paradigms, with the aim of providing a comprehensive approach to formal semantics. Our embedding in Isabelle, though essentially deep, integrates with Isabelle/HOL type checking and proof tactics, thus providing a powerful platform for UTP proof.
This work is partly supported by EU FP7
(grant agreement 287829).
Comprehensive Modelling for Advanced Systems of Systems