Coinduction for Verification and Certification
The aim of this ERC project is to exploit the unsung power of coinduction to improve upon the state of the art in verification and certification. The project is rather open-ended and goes from theory (category theory, coinduction) to practice (concrete implementations and linking with existing software). We plan to work on the following topics:
|Automata algorithms||Calculus of relations||Proof assistants (Coq)|
Together with Filippo Bonchi, we have recently found a new
algorithm for language equivalence of finite automata on
strings . This algorithm
exploits bisimulations up to congruence, and improves
existing algorithms by an order of magnitude.
Here we study the theory of binary relations and their
standard operations (union, composition, transitive closure,
Proof assistants should help the user to write its proof.
To this end, one needs to provide powerful automation tools.
By certifying our results about automata and the calculus of relations, we aim at