Isabelle/UTP

Isabelle/UTP is a collection of tools, built on top of the Isabelle/HOL proof assistant, for building practical verification tools. It applies the principles of Hoare and He's Unifying Theories of Programming semantic framework to support formal semantics for a host of heterogeneous languages and notations. This is supported by Isabelle's highly extensible interface and open architecture, which allows us to embed a variety of DSLs, and apply an array of integrated automated verification tools (notably sledgehammer).

In the accompanying image, you can see a simple example: an imperative algorithm for list reversal, which can be symbollically executed and verified using a total correctness Hoare logic. However, Isabelle/UTP is not limited to simple imperative programs, but supports an array of software engineering paradigms, including state-based notations (such as RoboChart), concurrent and reactive programming, and cyber-physical systems.