Abstract

Kleene algebra with tests 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.

This tutorial 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 frameworks for program verification, including successful extensions and fundamental limitations.

Context

Computer scientists have long explored the connections between families of programming languages and abstract machines. This dual perspective has furnished deep theoretical insights as well as practical tools. As an example, Kleene’s classic result establishing the equivalence of regular expressions and finite automata inspired decades of work across a variety of areas including programming language design, mathematical semantics, and formal verification.

Kleene Algebra with Tests (KAT), which combines Kleene Algebra (KA) with Boolean Algebra (BA), is a modern example of this approach. Viewed from the program-centric perspective, a KAT models the fundamental constructs that arise in programs: sequencing, branching, iteration, non-determinism, etc. The equational theory of KAT enables algebraic reasoning and can be finitely axiomatized. Viewed from the machine-centric perspective, a KAT describes a kind of automaton that generates a regular language of traces. This shift in perspective admits techniques from the theory of coalgebras for reasoning about program behavior. In particular, there are efficient algorithms for checking bisimulation, which can be optimized using properties of bisimulations or symbolic automata representations.

KAT has been used to model computation across a wide variety of areas including program transformations, concurrency control, compiler optimizations, cache control, and more. A prominent recent application is NetKAT, a language for reasoning about the packet-forwarding behavior of software-defined networks. NetKAT has a sound and complete equational theory, and a coalgebraic decision procedure that can be used to automatically verify properties such as reachability, loop-freedom, and isolation.

Objective

The objective of this tutorial is to provide attendees with a comprehensive introduction to Kleene Algebra with Tests (KAT) including techniques for using KAT to model and reason about computation in a variety of domains.

Topics

The tutorial will cover the following topics:

1. Basics: syntax, denotational semantics, axiomatization and decision procedure for Kleene Algebra and KAT.
2. Applications: using KAT to establish the correctness of a program transformations including the Bohm-Jacopini theorem and the NetKAT to OpenFlow compiler.
3. Extensions: systems obtained by enriching KAT with additional equations including NetKAT and KAT+B!
4. Limits: fundamental limits on decidability and systems that go beyond the decidable fragment

Presenters

Dexter Kozen is the Joseph Newton Pew, Jr. Professor in Engineering, at Cornell University. One of the fathers of dynamic logic and the Mu-calculus, he is also credited for a number of major contributions in logic, theory of computation, automata theory and computational complexity. Dexter is a Fellow of the Association for Computing Machinery, a Guggenheim Fellow, and has received numerous awards, including an Outstanding Innovation Award from IBM, the EATCS award, and the honor of a professorship at The Radboud Excellence Initiative, in the Netherlands.

Nate Foster is an Associate Professor of Computer Science at Cornell University and a Principal Research Engineer at Barefoot Networks. The goal of his research is to develop languages and tools that make it easy for programmers to build secure and reliable systems. His current work focuses on the design and implementation of languages for programming software-defined networks. In the past he has also worked on bidirectional languages (also known as “lenses”), database query languages, data provenance, type systems, mechanized proof, and formal semantics. He received a PhD in Computer Science from the University of Pennsylvania. His honors include a Sloan Research Fellowship, an NSF CAREER Award, a Most Influential POPL Paper Award, and the SIGCOMM Rising Star Award.

Alexandra Silva is a Professor of Algebra, Semantics, and Computation at University College London. Her main research focuses on semantics of programming languages and modular development of algorithms for computational models. Much of her work uses the unifying perspective offered by coalgebra, a mathematical framework established in the last decades. She was the recipient of the 2018 Needham Award, 2017 Presburger Award, 2016 Leverhulme Prize, and 2015 ERC starting Grant.