Kleene algebra with tests (KAT) is a system for describing and manipulating computations and assertions. KAT allows propositional logic and the algebra of programs to be integrated seamlessly into a single system that is remarkably powerful in expressive and deductive power, yet computationally and conceptually simple.
KAT has many applications in computer science. In particular it has recently been used to specify and verify various communication protocols and common compiler optimizations. It does so more simply and with less effort than more traditional systems such as Hoare Logic.
In this proposal, we propose (i) to further develop the theory of KAT; (ii) to produce a research monograph of significant scope giving a comprehensive introduction to KAT; and (ii) to continue to investigate the use of KAT in practical program verification.
