hal-00665995, version 1
A non-local method for robustness analysis of floating point programs
Ivan Gazeau
a, 1, 2Dale Miller
1, 3Catuscia Palamidessi
a, 1, 2
QAPL - Tenth Workshop on Quantitative Aspects of Programming Languages (2012)
Résumé : Robustness is a standard correctness property which intuitively means that if the input to the program changes less than a fixed small amount then the output changes only slightly. This notion is useful in the analysis of rounding error for floating point programs because it helps to establish bounds on output errors introduced by both measurement errors and by floating point computation. Compositional methods often do not work since key constructs---like the conditional and the while-loop---are not robust. We propose a method for proving the robustness of a while-loop. This method is non-local in the sense that instead of breaking the analysis down to single lines of code, it checks certain global properties of its structure. We show the applicability of our method on two standard algorithms: the CORDIC computation of the cosine and Dijkstra's shortest path algorithm.
- a – INRIA
- 1 : Laboratoire d'informatique de l'école polytechnique (LIX)
- CNRS : UMR7161 – Polytechnique - X
- 2 : COMETE (INRIA Saclay - Ile de France)
- INRIA – Polytechnique - X – CNRS : UMR7161
- 3 : PARSIFAL (INRIA Saclay - Ile de France)
- INRIA – Polytechnique - X – CNRS : UMR7161
- Domaine : Informatique/Langage de programmation
- Mots-clés : Program analysis – floating-point arithmetic – robustness to errors.
- hal-00665995, version 1
- http://hal.inria.fr/hal-00665995
- oai:hal.inria.fr:hal-00665995
- Contributeur : Dale Miller
- Soumis le : Vendredi 3 Février 2012, 12:45:09
- Dernière modification le : Vendredi 3 Février 2012, 14:16:34






Documents associés

Exporter