Kleene Algebra

点击翻译按钮获取中文摘要

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.