Software Components for Verified Scientific Computation

Project: Arenaire
Research Director (HDR): Gilles Villard (LIP-CNRS), Gilles.Villard@ens-lyon.fr
Co-director: Nathalie Revol (LIP-INRIA), Nathalie.Revol@ens-lyon.fr

Scientific context
This doctoral project will take place within the project Arenaire, located in the LIP laboratory. The research of Arenaire focuses on computer arithmetic. The goal of this doctoral project is to contribute to the development of certified computations in scientific computing and mainly in linear algebra. Several approaches will be taken, based on floating-point arithmetic and interval arithmetic, or on exact arithmetic. More precisely:

• arbitrary precision interval arithmetic and dedicated numerical algorithms, which lead to certified numerical results while still using floating-point arithmetic;
• exact arithmetic especially for finite fields, rational numbers or polynomials.

Doctoral Subject
The candidate will work on these topics, including both algorithm design and software realizations. The algorithm side may concern linear algebra, lattice basis reduction, numerical constraint programming or optimization. The softwares developed during the PhD will be integrated within existing libraries such as LinBox or MPFI. Applications are foreseen in control theory.

Method and Expected Results
The following approaches will be investigated, to solve problems of linear algebra in particular :

• take fully advantage of the computing precision (in floating-point arithmetic) to get results as accurate as if they were computed using twice this precision: accurate dot product, iterative refinement, etc.; (Cf. Chapter 7 on Iterative refinement, N. Higham: Accuracy and Stability of Numerical Algorithms, SIAM Press, 2nd edition, 2003, and more recent results by the same author, to get an idea of possible theoretical results for the problem of solving a linear system.)
• to solve problems using multiple-precision interval arithmetic, iterative refinement (or more generally, contractant iteration) is promising; the precision should be automatically adapted when necessary, but it is an issue to detect automatically when it is necessary to increase the precision; (Cf. N. Revol: Interval Newton iteration in multiple precision for the univariate case, Numerical Algorithms, vol 34, no 2, pp 417--426, 2003 for a specific problem, or K.O. Geddes and W.W. Zheng: Exploiting fast hardware floating point in high precision computation, Proceedings ISSAC 2003, pp 111-118, for experimental results on several problems, in arbitrary precision floating-point -- but not interval -- arithmetic.)
• solving problems exactly, i.e. with an arbitrary precision, could also benefit of accurate results, computed with floating-point arithmetic, along with certificates on these results to guarantee that the floating-point result is indeed the exact (integer for instance) sought result. (Cf. S. Rump: Computer-Assisted Proofs and Self-Validating Methods, pp. 195--240, in B. Einarsson, editor: Handbook of Accuracy and Reliability in Scientific Computation, SIAM, 2005, or G. Villard. Certification of the QR factor R, and of lattice basis reducedness, LIP RR2007-03, hal-00127059, 2007.)

How to apply
Send your vitae and the names and addresses, including email, of three reference persons (three persons who can write a recommendation letter) to Gilles.Villard@ens-lyon.fr, Nathalie.Revol@ens-lyon.fr, with "PhD thesis application" as subject.