NSCPHD1238 Introduction to Kleene Algebra and Kleene Algebra with Tests
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.
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.
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.
https://intranet.ku.dk/computerscience_ma/electives/preapproval/Pages/default.aspx for information.
- Category
- Hours
- Exercises
- 100
- Lectures
- 30
- Preparation
- 76
- Total
- 206
Registration: jettegm@di.ku.dk.
- Credit
- 7,5 ECTS
- Type of assessment
- Continuous assessmentActive 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.
Course information
- Language
- English
- Course code
- NSCPHD1238
- Credit
- 7,5 ECTS
- Level
- Ph.D.
- Duration
- 1 block
- Placement
- Block 3
- Schedule
- A (Tues 8-12 + Thurs 8-17)
- Course capacity
- No limit
- Study board
- Natural Sciences PhD Committee
Contracting department
- Department of Computer Science
Course responsibles
- Fritz Henglein (8-6a6770696e676b7042666b306d7730666d)
Lecturers
Dexter Kozen, guest professor from Cornell University