Kleene Algebra

带有测试的Kleene代数（KAT）是一个描述和操作计算和断言的系统。 KAT允许命题逻辑和程序代数无缝地集成到一个具有强大的表达能力和演绎能力，但计算和概念简单的单一的程序中。 特别是它最近已被用来指定和验证各种通信协议和常见的编译器优化。 它这样做更简单，更少的努力比更传统的系统，如HoareLogic.In这一建议，我们建议（i）进一步发展的理论KAT;（ii）产生一个研究专著的重要范围给予全面介绍KAT;和（ii）继续investigatethe使用KAT在实际程序验证。

Kleene algebra with tests (KAT) is a system for describing andmanipulating computations and assertions. KAT allows propositional logicand the algebra of programs to be integrated seamlessly into a singlesystem that is remarkably powerful in expressive and deductivepower, yet computationally and conceptually simple.KAT has many applications in computer science. In particularit has recently been used to specify and verify various communicationprotocols and common compiler optimizations. It does so more simplyand with less effort than more traditional systems such as HoareLogic.In this proposal, we propose (i) to further develop the theory of KAT;(ii) to produce a research monograph of significant scope giving acomprehensive introduction to KAT; and (ii) to continue to investigatethe use of KAT in practical program verification.