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.
The following students have contributed to this project:
 | Kamal Aboul-Hosn | KAT-ML theorem prover |
| Nikita Kuznetsov | KAT-ML theorem prover |
| Chris Hardin | Theory of KA and KAT |
| NuPrl |
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