Kleene algebra modulo theories: a framework for concrete KATs

Michael Greenberg, Ryan Beckett, Eric Campbell

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

5 Scopus citations

Abstract

Kleene algebras with tests (KATs) offer sound, complete, and decidable equational reasoning about regularly structured programs. Interest in KATs has increased greatly since NetKAT demonstrated how well extensions of KATs with domain-specific primitives and extra axioms apply to computer networks. Unfortunately, extending a KAT to a new domain by adding custom primitives, proving its equational theory sound and complete, and coming up with an efficient implementation is still an expert's task. Abstruse metatheory is holding back KAT's potential. We offer a fast path to a "minimum viable model"of a KAT, formally or in code through our framework, Kleene algebra modulo theories (KMT). Given primitives and a notion of state, we can automatically derive a corresponding KAT's semantics, prove its equational theory sound and complete with respect to a tracing semantics (programs are denoted as traces of states), and derive a normalization-based decision procedure for equivalence checking. Our framework is based on pushback, a generalization of weakest preconditions that specifies how predicates and actions interact. We offer several case studies, showing tracing variants of theories from the literature (bitvectors, NetKAT) along with novel compositional theories (products, temporal logic, and sets). We derive new results over unbounded state, reasoning about monotonically increasing, unbounded natural numbers. Our OCaml implementation closely matches the theory: users define and compose KATs with the module system.

Original languageEnglish
Title of host publicationPLDI 2022 - Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation
EditorsRanjit Jhala, Isil Dillig
Pages594-608
Number of pages15
ISBN (Electronic)9781450392655
DOIs
StatePublished - 9 Jun 2022
Event43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2022 - Virtual, Online, United States
Duration: 13 Jun 202217 Jun 2022

Publication series

NameProceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)

Conference

Conference43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2022
Country/TerritoryUnited States
CityVirtual, Online
Period13/06/2217/06/22

Keywords

  • algebraic models
  • program equivalence
  • tracing semantics
  • verification

Fingerprint

Dive into the research topics of 'Kleene algebra modulo theories: a framework for concrete KATs'. Together they form a unique fingerprint.

Cite this