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 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.

News

Next postdoc/PhD positions expected to start September 2018; please write to me directly if you could be interested.

References

  1. Hacking Nondeterminism with Induction and Coinduction, .pdf
    F. Bonchi and D. Pous, Research Highlights in Communications of the ACM, Vol. 58 No. 2, 2015.
    Associated web page.

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

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

A few more references and scientific details can be found on the following page for Master 2 internships proposals.



CNRS ENS de Lyon Université de Lyon ERC European Union