Kleene Algebra with Tests and Coq Tools for While Programs

Damien Pous (1, 2)

1 LIP - Laboratoire de l'Informatique du Parallélisme
2 PLUME - Preuves et Langages

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.

Mots clés: program verification; Kleene algebra with tests; KAT; Decision procedure; regular expressions; Coq; while programs; Hoare logic

Domaines: Logique en informatique [cs.LO]; Langage de programmation [cs.PL]; Logiciel mathématique [cs.MS]

Damien Pous. Kleene Algebra with Tests and Coq Tools for While Programs. Interactive Theorem Proving 2013, Jul 2013, Rennes, France. pp.180-196, ⟨10.1007/978-3-642-39634-2_15⟩. ⟨hal-00785969⟩