Algebras for Program Correctness in Isabelle/HOL

We present a reference formalisation of Kleene algebra and demonic refinement algebra with tests in Isabelle/HOL. It provides three different formalisations of tests. Our structured comprehensive libraries for these algebras extend an existing Kleene algebra library. It includes an algebraic account of Hoare logic for partial correctness and several refinement and concurrency control laws in a total correctness setting. Formalisation examples include a complex refinement theorem, a generic proof of a loop transformation theorem for partial and total correctness and a simple prototypical verification tool for while programs, which is itself formally verified.