23rd Estonian Winter School in Computer Science (EWSCS)
XXIII Eesti Arvutiteaduse Talvekool

Palmse, Estonia, March 4 - 9, 2018

Georg Struth

Dept. of Computer Science
University of Sheffield

Introduction to Kleene algebra


Kleene algebras were proposed originally as axiom systems for the equational theory of regular expressions. Yet beyond their place in theoretical computer science, they have been used widely in computational modelling, in particular program construction and verification. This lecture series introduces some of the most prominent variants, including Kleene algebras with tests, modal Kleene algebras and concurrent Kleene algebras, and discusses some typical applications.

After a brief historical overview, I introduce Kozen's axiom system for Kleene algebra, discuss some computationally interesting models and present Kozen's completeness proof with respect to the equational theory of regular expressions. Then I show shown how Kleene algebras with tests allow one to model simple while programs and to verify them in algebraic approaches to Hoare logic and Morgan's refinement calculus. Next I present modal Kleene algebras, point out connections to dynamic logics and predicate transformer semantics, and discuss additional applications in program analysis and verification. Finally, I introduce concurrent Kleene algebra together with its most important models, and outline some directions for future research.

Program verification components based on variants of Kleene algebra and formalised with the Isabelle/HOL proof assistant will be presented during the lectures and explored in the exercise sessions.

Course materials

Valid CSS! Valid XHTML 1.0 Strict Last changed April 10, 2020 22:36 Europe/Helsinki (GMT +03:00) by local organizers, ewscs18(at)cs.ioc.ee
EWSCS'18 page: http://cs.ioc.ee/ewscs/2018/