NSCPHD1238 Introduction to Kleene Algebra and Kleene Algebra with Tests

Volume 2014/2015
Content

Kleene algebra (KA) is the algebra of regular expressions. It captures axiomatically the properties of many structures arising in computer science. It is named for Stephen Cole Kleene (1909-1994), who among his many other achievements invented finite automata and regular expressions. KA is the algebraic theory of these objects, although it has many other natural and useful interpretations. Kleene algebras arise in various guises in many contexts: relational algebra, semantics and logics of programs, automata and formal language theory, and the design and analysis of algorithms.

Kleene algebra with tests (KAT) is Kleene algebra augmented with Boolean tests. The tests allow the modeling of common imperative programming language constructs and partial correctness assertions. KAT provides an equational approach to program verification that subsumes traditional approaches such as Hoare logic. It has proven successful in many application in static analysis and program verification: lazy caching, concurrency control, low-level compiler optimizations, data restructuring operations in parallelizing compilers, and pointer analysis, to name a few. A recent success is NetKAT, a system that augments KAT with primitives for reasoning about packet switching networks.

In this course, we will develop the basic algebraic theory of KA and KAT, along with applications in program verification and static analysis. We will give several examples of Kleene algebras - relational models, language models, trace models, matrix algebras - and describe their uses. We will review the various axiomatizations and discuss their relationship. We will develop a decision algorithm for the equational theory and prove that the standard axiomatization is deductively complete over language and relational models. We will also develop the coalgebraic theory, which gives rise to efficient decision procedures. As a final application we will describe NetKAT, a system based on KAT that has been incorporated as part of the Frenetic suite of network management tools. We will show how NetKAT can be used to specify and verify various network properties such as reachability, cycle-freedom, and isolation.

 

Learning Outcome

Knowledge:

Basic theory of Kleene algebra (KA) and Kleene algebra with tests (KAT); models and axiomatizations of their equational theories; coalgebraic theory and efficient decision procedures for KA and KAT.

Skills:

Apply KA and KAT to problems in computer science such as concurrency control, low-level compiler optimizations, data restructuring, pointer analysis and software-defined networks.

Competences:

Mathematical modeling of and equational reasoning for software systems to prove safety and correctness and to improve their performance.

Lecture notes and papers from the scientific literature.

Familiarity with basic algebra and logic, automata theory, basic complexity theory, and design and analysis of algorithms.
Lectures plus written exercises.

Lectures take place Tuesdays and Thursdays, 9:15-12 a.m. in Universitetparken 1, room 1-0-22 and 1-0-14, respectively, first time February 3rd.
If you are MS student satisfying the stipulated academic qualifications you are welcome to take the course. To do so, you need to get preapproval from the Study Board for Mathematics and Computer Science. See
https:/​/​intranet.ku.dk/​computerscience_ma/​electives/​preapproval/​Pages/​default.aspx for information.
  • Category
  • Hours
  • Exercises
  • 100
  • Lectures
  • 30
  • Preparation
  • 76
  • Total
  • 206
Credit
7,5 ECTS
Type of assessment
Continuous assessment
Active participation in class, plus weekly homework sets of 4-5 problems each.
Marking scale
passed/not passed
Censorship form
No external censorship
Several internal examiners
Re-exam
Resubmission of mandatory assignments (written exercises), plus 30 minutes' oral exam without preparation.
Criteria for exam assesment

Active participation in class, plus acceptable answers to at least 50% of the weekly homework sets.