A non-local method for robustness analysis of floating point programs

Ivan Gazeau 1, 2, * Dale Miller 1, 3 Catuscia Palamidessi 1, 2
* Auteur correspondant
2 COMETE - Concurrency, Mobility and Transactions
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR7161
3 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR7161
Abstract : 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.
Type de document :
Communication dans un congrès
Mieke Massink and Herbert Wiklicky. QAPL - Tenth Workshop on Quantitative Aspects of Programming Languages, Mar 2012, Tallinn, Estonia. Open Publishing Association, 8555, pp.63-76, 2012, EPTCS. 〈10.4204/EPTCS.85.5〉
Liste complète des métadonnées

Littérature citée [11 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00665995
Contributeur : Dale Miller <>
Soumis le : lundi 9 juillet 2012 - 09:25:18
Dernière modification le : jeudi 10 mai 2018 - 02:06:40
Document(s) archivé(s) le : mercredi 10 octobre 2012 - 02:21:55

Fichiers

proof_example.pdf
Fichiers éditeurs autorisés sur une archive ouverte

Identifiants

Collections

Citation

Ivan Gazeau, Dale Miller, Catuscia Palamidessi. A non-local method for robustness analysis of floating point programs. Mieke Massink and Herbert Wiklicky. QAPL - Tenth Workshop on Quantitative Aspects of Programming Languages, Mar 2012, Tallinn, Estonia. Open Publishing Association, 8555, pp.63-76, 2012, EPTCS. 〈10.4204/EPTCS.85.5〉. 〈hal-00665995v3〉

Partager

Métriques

Consultations de la notice

528

Téléchargements de fichiers

117