CerPAN

Financed project by the Agence Nationale de la Recherche.

This project aims at developing and applying methods which allow us to formally prove the soundness of programs from numerical analysis. In particular, we are interested in programs which often appear in the resolution of critical problems. Many critical programs come from numerical analysis, but few people have ever tried to apply formal methods to this kind of programs. The main reason is that real numbers (floating-point) are greatly used in numerical programs, whereas formal methods tend to handle integers, or more generally discrete structures.

However, the tools for formal methods and in particular the formal proof systems are more and more appropriate these days to deal with the family of real numbers (floating-point numbers, exact-real numbers), which makes it possible to apply these systems to numerical analysis programs. Two methods are investigated in this project.
The first one consists in using tools based on Why such as Caduceus. The idea is to work on a existing program, which is annoted w.r.t. the properties we want to be preserved. These annotations generate some proof obligations for several proof systems. These tools, developed by some of the members of this project, do not deal with floating-point numbers yet. A first step of this project will consist in extending these tools to floating-point numbers.

The other method is to carry out the formalization as well as the proof of the problem, and to use the principle of extraction of the Coq system to automatically get a sound (proved) program. This principle of extraction does not deal with the family of real numbers, and another step of this project will consist to understand how to extend extraction to this family of numbers.

These two methods require some techniques regarding proof automation, in order to make our methods available and especially usable by non-experts in formal proofs. In an additional way, we will try to be aware of the notions of efficiency, which may be crucial in numerical analysis in particular. The methods developed in this project may be applied to a large variety of problems in environments intended to produce numerical code, which is safe and correct w.r.t. its formal specification. The project is the association of several members with varied and appropriate competences (numericians, experts in proof assistant design, in proofs of programs, in real and floating-point numbers) and with a significant experience in their respective domains.