# Kleene Algebra with Tests and Coq Tools for While Programs

arXiv: https://arxiv.org/abs/1302.1737 · HTML: https://mlsanity.com/paper/1302.1737/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 7 Feb 2013.

## Built on by (most cited first, 1 of 1)

- [On Incorrectness Logic and Kleene Algebra with Top and Tests](https://mlsanity.com/paper/2108.07707/) (2021)

## Abstract (arXiv)

We present a Coq library about Kleene algebra with tests, including a proof of their completeness over the appropriate notion of languages, a decision procedure for their equational theory, and tools for exploiting hypotheses of a particular shape in such a theory. Kleene algebra with tests make it possible to represent if-then-else statements and while loops in most imperative programming languages. They were actually introduced by Kozen as an alternative to propositional Hoare logic. We show how to exploit the corresponding Coq tools in the context of program verification by proving equivalences of while programs, correctness of some standard compiler optimisations, Hoare rules for partial correctness, and a particularly challenging equivalence of flowchart schemes.