# Kleene algebra, from automata algorithms to proof assistants

Damien Pous ( CNRS, ENS Lyon )

- 11:00 11th May 2016 ( Trinity Term 2016 )441

Kleene algebra are the algebraic counterpart to finite automata on finite words.

First I will describe two recent algorithms for finite automata: one

exploiting bisimulations up to congruence to tame non-determinism, and

one exploiting binary decision diagrams to handle large alphabets.

Then I will show how such algorithms can be used to provide powerful

automation tools in a proof assistant like Coq, in particular in for

program certification.