Kleene Algebra with Tests (KAT)

Kleene algebra with tests (KAT) is an equational system for program verification that combines Kleene algebra (KA) with Boolean algebra. KAT has been applied successfully in various low-level verification tasks involving communication protocols, basic safety analysis, source-to-source program transformation, concurrency control, compiler optimization, and static analysis. The system subsumes Hoare logic and is deductively complete for partial correctness over relational models.

KAT-ML is an interactive theorem prover for Kleene algebra with tests. The system is designed to reflect the natural style of reasoning with KAT that one finds in the literature. It is available for several platforms.

Selected Sources

Dexter Kozen. A completeness theorem for Kleene algebras and the algebra of regular events. Infor. and Comput., 110:366-390, May 1994.
Dexter Kozen. On Hoare logic and Kleene algebra with tests. Proc. IEEE Conf. Logic in Computer Science (LICS'99), IEEE, July 1999, 167-172.  Trans. Computational Logic 1:1 (July 2000), 60-76.
Course notes, CS786 Spring 04, Introduction to Kleene Algebra
Kamal Aboul-Hosn and Dexter Kozen. KAT-ML: An Interactive Theorem Prover for Kleene Algebra with Tests. In Boris Konev and Renate Schmidt, editors, Proc. 4th Int. Workshop on the Implementation of Logics (WIL'03), 2-12. University of Manchester, September 2003.



The following students have contributed to this project:

Kamal Aboul-HosnKAT-ML theorem prover
Nikita KuznetsovKAT-ML theorem prover
Chris HardinTheory of KA and KAT

Related Projects at Cornell



This work was supported in part by NSF grant CCR-0105586 and by ONR Grant N00014-01-1-0968. The views and conclusions contained herein are those of the author and should not be interpreted as necessarily representing the official policies or endorsements, either expressed or implied, of these organizations or the US Government.

Send email to Dexter
Dexter's home page
Copyright (c) 2004 Cornell University
Last updated: 25 January 2018