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.

• Concrete and abstract semantics of floating-point operations


• Static analysis of programs by abstract interpretation

General Context Principle of the analysis Presentation of the FLUCTUAT analyzer Bibliography of the project

• Eric Goubault,  email: eric.goubault@cea.fr


• Matthieu Martel, email: matthieu.martel@cea.fr


• Sylvie Putot, email: sylvie.putot@cea.fr

• 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

 

Back to the LSL laboratory