Verification with Unifying Theories
Hoare and He’s Unifying Theories of Programming is a framework for construction of denotational semantic meta-models for a variety of programming languages based on an alphabetised relational calculus. Isabelle/UTP is an implementation of their framework based in Isabelle/HOL. It can be used to formalise semantic building blocks for programming language paradigms (based on UTP theories), prove algebraic laws of programming, and then use these laws to construct program verification tools.
Isabelle/UTP can thus be used to build verification tools for a variety paradigms. Currently we have support for simple relational programs (as illustrated below), and stateful reactive programs in Circus. We are also working on theories of hybrid and Cyber-Physical systems.
Isabelle/UTP is supported by projects INTO-CPS, RoboCalc, and CyPhyAssure