25 Years of KAT

Kleene algegra with tests (KAT) is a system for equational reasoning about imperative programs. The system is based on Kleene algebra, the algebra of regular expressions. In this talk I will trace the origins of the system and survey past and recent results on expressiveness, decision complexity, and deductive completeness, along with various applications, including correctness of compiler optimizations and verification of packet switching networks.

Authors

• Dexter Kozen

Keywords

No keywords are indexed for this paper.