Kleene Algebra

Kleene代数与测试（KAT）是一个描述和操作计算和断言的系统。KAT允许命题逻辑和程序的代数无缝地集成到一个系统中，该系统在表达和演绎能力方面非常强大，但在计算和概念上却很简单。KAT在计算机科学中有许多应用。特别是最近被用来指定和验证各种通信协议和常见的编译器优化。它比HoareLogic等传统系统更简单、更省力。在本提案中，我们提出(i)进一步发展KAT理论；（ii）制作一份范围广泛的研究专著，全面介绍KAT；（ii）继续调查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.