Section: New Results

Certification of Algorithms, Languages, Tools and Systems

Case study: Matrix Multiplication.

M. Clochard, L. Gondelman and M. Pereira wrote a paper describing a complete solution for the first challenge of the VerifyThis 2016 competition held at the 18th ETAPS Forum, where they obtain the award for the best student team. Two variants for the multiplication of matrices are presented and proved: a naive version using three nested loops and Strassen's algorithm. To formally specify the two multiplication algorithms, they developed a new Why3 theory of matrices, and they applied a reflection methodology to condut some of the proofs. This work was presented at the VSTTE Conference [21]. An extended version that considers arbitrary rectangular martices instead of square ones is in preparation. The development is available at http://toccata.lri.fr/gallery/verifythis_2016_matrix_multiplication.en.html.

Case study: Koda-Ruskey's algorithm for generating ideals of a forest.

J.-C. Filliâtre and M. Pereira presented the first formal proof of an implementation of Koda and Ruskey's algorithm (an algorithm for generating all ideals of a forest poset as a Gray code) at VSTTE 2016 [23]. The proof is conducted within the Why3 system and is mostly automatic.

The Lax-Milgram Theorem.

S. Boldo, F. Clément, F. Faissole, V. Martin, and M. Mayero have worked on a Coq formal proof of the Lax–Milgram theorem. The Finite Element Method is a widely-used method to solve numerical problems coming for instance from physics or biology. To obtain the highest confidence on the correction of numerical simulation programs implementing the Finite Element Method, one has to formalize the mathematical notions and results that allow to establish the sound-ness of the method. The Lax–Milgram theorem may be seen as one of those theoretical cornerstones: under some completeness and coercivity assumptions, it states existence and uniqueness of the solution to the weak formulation of some boundary value problems. This article presents the full formal proof of the Lax–Milgram theorem in Coq. It requires many results from linear algebra, geometry, functional analysis , and Hilbert spaces. This has been published at the 6th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2017) [18].

ALEA library extended with continuous datatypes

The ALEA library uses a monadic construction to formalize discrete measure theory. F. Faissole and B. Spitters proposed to extend it to continuous datatypes. They used both synthetic topology and homotopy type theory to achieve the formalization. This work is presented at the Workshop on Coq for Programming Languages [32].

Case study: Strongly Connected Components of a Graph

R. Chen and J.-J. Lévy designed a formal proof of Tarjan's algorithm for computing the strongly connected component of a directed graph. The proof is conducted using Why3. This work is presented at the JFLA conference [28]. This case study is part of a larger set of case studies on algorithms on graphs http://pauillac.inria.fr/~levy/why3/.

Case study: Unix Pathname Resolution

R. Chen, M. Clochard and C.-Marché designed a formal proof of an algorithm for resolving a pathname in Unix file systems. The proof is conducted using Why3 [34]. This case study is part of the CoLiS project.