logo

CoVeCe

Coinduction for Verification and Certification

Damien Pous

logo

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 [1]. This algorithm exploits bisimulations up to congruence, and improves existing algorithms by an order of magnitude.
  • Can we extend this idea to more challenging automata models? (alternating, tree, push-down, Büchi...)
  • Can we mix this idea with symbolic approaches for handling huge state-spaces?
Here we study the theory of binary relations and their standard operations (union, composition, transitive closure, converse...).
  • Can we decide the equational theory?
  • Can we axiomatise it?
  • Can we design proof systems for it? (e.g., using non-commutative linear logic)
We obtained encouraging preliminary results with Paul Brunet [2], where we use Petri automata to recognise regular sets of directed graphs. Many directions remain to be explored.
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
  • bringing standard verification techniques into the realm of proof assistants;
  • providing a comprehensive library for binary relations (i.e., further extending [3]).
As an additional outcome, we expect to distribute certified implementations of automata algorithms and verification tools.

Team

Close collaborators

  • Filippo Bonchi
  • Adrien Durier
  • Daniel Hirschkoff
  • Denis Kuperberg
  • Olivier Laurent
  • Matteo Mio
  • Jurriaan Rot
  • Davide Sangiorgi

References

  1. Hacking Nondeterminism with Induction and Coinduction, .pdf
    Filippo Bonchi and Damien Pous,
    Research Highlights in Communications of the ACM, 2015.
    Associated web page.

  2. Petri automata for Kleene allegories, .pdf.
    Paul Brunet and Damien Pous, in Proc. LICS'15.
    Associated web page.

  3. Kleene Algebra with Tests and Coq Tools for while Programs, .pdf.
    Damien Pous, in Proc. ITP'13.
    Associated Coq library,

Publications



CNRS ENS de Lyon Université de Lyon ERC European Union