# 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. |

| More papers |

### Personnel

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 |

### Related Projects at Cornell

### Acknowledgments

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

Send email to Kamal

Dexter's home page

Copyright (c) 2004 Cornell University

Last updated: 12 August 2004