Report

Teaser, summary, work performed and final results

Periodic Reporting for period 2 - CoVeCe (Coinduction for Verification and Certification)

Teaser

In critical application domains like aeronautics, distant surgerysystems, or cryptography, one needs to avoid bugs at all costs.Formal methods like verification provide automatic means of findingsome of these bugs. Certification, using proof assistants like Coq orIsabelle/HOL...

Summary

In critical application domains like aeronautics, distant surgery
systems, or cryptography, one needs to avoid bugs at all costs.

Formal methods like verification provide automatic means of finding
some of these bugs. Certification, using proof assistants like Coq or
Isabelle/HOL, make it possible to guarantee the absence of bugs (up to
a certain point).

These two kinds of tools are crucial in order to design safer programs
and machines. Unfortunately, state-of-the art tools are not yet
satisfactory. Verification tools often face state-explosion problems
and require more efficient algorithms; certification tools need more
automation: they currently require too much time and expertise, even
for basic tasks that could be handled easily through verification.

In this project, we look for new techniques, new algorithms, or new
tools, that will make it possible to verify and/or certify complex
systems that are currently out of reach.

Our approach is based on mathematics: we study mathematical structures
that make it possible to reason about programs, and we look for
algorithms that make it possible to analyse those structures
efficiently. We use several tools from mathematics and computer
science: abstract coinduction, universal coalgebra, proof theory,
graph theory.

Work performed

Kleene algebra are at the heart of the project: these algebraic
structures make it possible to represent programs abstractly, and
their equational theory can be decided using coinductive automata
algorithms. This is how we obtained automation tactics for program
verification in the Coq proof assistant. A substantial part of our
research is about understanding extensions of these structures.

We obtained several new results in that direction.

First, we obtained decidability of allegories, a finitely based
equational theory accounting for the most common operations on binary
relations: union, intersection, composition, and transpose. We used
graph theory techniques to solve this problem, which was open since
1995.

Second, we obtained a completness proof for a form of Kleene algebra
with intersection. There, this is the addition of the intersection
operation which is challenging: from the semantics point of view, it
requires us to move from languages of words, which enjoy a solid
tradition in computer science, to languages of graphs, whose theory is
much less developped.

Third, we managed to use tools from Logic (more precisely, proof
theory), in order to characterise various extensions of Kleene
algebra. This made it possible to provide new insights on those
theories, which we hope to exploit in the future to obtain new
decidability/completeness results.


Another area we explored is that of abstract coinduction. Indeed, this
mathematical tool is hidden behind several verification algorithms, so
that better understanding this concept can help to design new or
faster algorithms. There we did a breaktrhough by showing that
coinductive methods can be enhanced in a uniform way, using an object
called the companion. We further developped this theory using the
language of category theory (more specifically, universal coalgebra),
in order to widen its scope of applicability.


Lastly, an important aspect of the project is the formalisation in the
Coq proof assistant of some of the theories and algorithms mentioned
above. Indeed, we want in fine to provide certification tools, with
the highest degree of confidence. We already formalised several of our
results; one of them required us to develop a library for graph theory
in Coq, which we are now releasing.

Final results

By the end of the project, we hope to obtain completeness results for
Kleene allegories and other extenstions, as well as certified algorithms for those.

We also expect to obtain new coinductive automata algorithms and to release a
certified library of such algorithms.

Website & more info

More info: http://perso.ens-lyon.fr/damien.pous/covece/.