Title: Automating program equivalence proofs using Kleene algebra
Abstract:
Kleene algebra and their extensions can be seen as equational systems
for program verification. For instance, Kleene algebra with tests make
it possible to represent while programs abstractly, and to reason
about them in an algebraic way.
Such structures often have a decidable equational theory, which makes
it possible to automate reasoning steps. This is especially useful in
the context of proof assistants, where one would like to focus on the
most challenging steps of a proof, delegating the other steps to the
machine.
I will illustrate how this can be achieved in Coq for Kleene algebra
with tests. Then I will discuss extensions that would make it possible
to go beyond purely sequential languages.