TL;DR
This paper introduces Kleene algebra modulo theories (KMT), a framework that automatically derives sound and complete semantics for domain-specific Kleene algebras with tests, facilitating easier extension and implementation.
Contribution
It provides a formal, automatable method to create and reason about domain-specific KATs using pushback, enabling efficient equivalence checking and new theoretical results.
Findings
Automated derivation of semantics for KATs from primitives and state notions
Proved soundness and completeness of the derived KATs with respect to tracing semantics
Implemented a practical OCaml framework for defining and composing KATs
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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
