This course has two main topics:

• I will present simple semantics for imperative programs based on Kleene algebras with tests and modal Kleene algebras (time permitting), and concrete relational, state transformer and predicate transformer semantics over simple program store models, that are based on these algebras.
• I will show how this approach, from the algebras to prototypical program verification components, can be formalised with the Isabelle/HOL proof assistant. In fact, part of this course will be devoted to work with Isabelle.

The course thus addresses all those who would like to learn the basics of Hoare logics and predicate transformer semantics in a particularly simple and lightweight approach, and how to build simple program verification components in a proof assistant using a semantic approach based on a shallow embedding. Beyond that it emphasises an approach to formalising mathematics, both algebraic structures and their models, using the type classes of contemporary proof assistants.

Detailed lecture notes for the course can be found below. They contain a link to Isabelle theory templates leading from the algebras to the verification components mentioned, including some verification examples. These can be completed and expanded by the participants as an extended exercise.

Lecture Notes on Algebraic Approaches to Program Verification