Programming and Reasoning with Kleene Algebra with Tests
Nate Foster (Cornell University)
Programming and Reasoning with Kleene Algebra with Tests
Nate Foster (Cornell University)
These materials build on the contributions of many to the NetKAT project, especially Jules Jacobs, Tobias Kappé, Dexter Kozen, and Alexandra Silva.
Kleene algebra with tests (KAT) is an algebraic framework that can be used to reason about imperative programs. It has been applied across a wide variety of areas including program transformations, concurrency control, compiler optimizations, cache control, networking, and more. These lectures will provide an overview of Kleene Algebra with Tests, including the syntax, semantics, and the coalgebraic theory underlying decision procedures for program equivalence. We will illustrate how it can be used as a core framework for network verification, including successful extensions and fundamental limitations.
PLDI 2024 • DOI
Introduces KATch, a tool for fast symbolic verification of NetKAT programs, enabling efficient checking of program equivalence and other properties using symbolic automata techniques.
POPL 2020 • DOI
Introduces Guarded Kleene Algebra with Tests (GKAT), an efficient framework for verifying program equivalence based on the so-called guarded fragment of KAT.
ICFP 2015 • DOI
Presents a high-performance compiler for NetKAT that handles complex features like regular paths and virtual networks, significantly improving compilation times with optimizations like symbolic automata representations.
POPL 2015 • DOI
Presents a new algorithm for deciding equivalence of NetKAT programs by constructing finite automata (policy automata) for NetKAT terms. Despite NetKAT's equational theory being PSPACE-complete, shows the procedure is efficient in practice.
POPL 2014 • DOI
Introduces NetKAT, a network programming language grounded in Kleene Algebra with Tests (KAT), providing a sound and complete equational theory for reasoning about network behavior.
APLAS 2014 • DOI
An accessible survey and tutorial of NetKAT's design and theory, providing a self-contained introduction to NetKAT's syntax, semantics, and equational reasoning principles.