Tuesday 22nd August, MORNING SESSION
Georg Struth, University of Sheffield
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.
BACKGROUND:
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.
PREPARATION:
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
SPEAKER:
Georg Struth is a Professor of Theoretical Computer Science and Head of the Verification research group at the University of Sheffield. Georg works mainly on logical and algebraic methods in computer science, formalised mathematics with interactive theorem provers and program verification and correctness. His interests range from foundational work on the axiomatisation and semantics of sequential and concurrent computing systems to applications in the design and implementation of program verification software.