The manipulation of real numbers by computers is approximated by floating-point
arithmetic, which uses a finite representation of numbers. This implies that
a (small in general) rounding error may be committed at each operation.
Although this approximation is accurate enough for most applications, there
are some cases where results become irrelevant because of the precision lost
at some stages of the computation, even when the underlying numerical scheme
is stable.
Our aim is to study the propagation of rounding errors in floating-point computations,
to automatically detect a possible catastrophic loss of precision, and its
source. We are developing a static analyzer,
intended to cope with real industrial problems, and we believe it is especially
appropriate for critical instrumentation software.
Research Areas
- Concrete and abstract semantics of floating-point operations
- Static analysis of programs by abstract interpretation
Our Approach
People
Projects
- 2000-2002 : RTD project IST-1999-20527 DAEDALUS of the European FP5
programme

- 2003-2004 : project "Preuves Approchées", supported by
the Direction des Programmes de l'Aviation Civile (DPAC)
- 2004 : Action Spécifique Validation numérique pour
le calcul embarqué (GDR ARP, CNRS-STIC)
- 2004-2005: ACI-SI
V3F : Validation et Vérification en
Présence de Calculs à Virgule Flottante
|