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.)
Software aspects will include the implementation of the proposed algorithms,
based on existing components: they will be parts of
MPFI and/or LinBox in particular. Another important issue is
the extension of their interoperability.
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.