• A non-local method for robustn...

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

Title:
A non-local method for robustness analysis of floating point programs
Authors:
Gazeau, Ivan, Miller, Dale, Palamidessi, Catuscia
Contributors:
Laboratoire d'informatique de l'École polytechnique [Palaiseau] (LIX), École polytechnique (X), Institut Polytechnique de Paris (IP Paris)-Institut Polytechnique de Paris (IP Paris)-Centre National de la Recherche Scientifique (CNRS), Concurrency, Mobility and Transactions (COMETE), Institut Polytechnique de Paris (IP Paris)-Institut Polytechnique de Paris (IP Paris)-Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X), Institut Polytechnique de Paris (IP Paris)-Institut Polytechnique de Paris (IP Paris)-Centre National de la Recherche Scientifique (CNRS)-Centre Inria de l'Institut Polytechnique de Paris, Centre Inria de Saclay, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre Inria de Saclay, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Proof search and reasoning with logic specifications (PARSIFAL), Institut Polytechnique de Paris (IP Paris)-Institut Polytechnique de Paris (IP Paris)-Centre National de la Recherche Scientifique (CNRS)-Centre Inria de Saclay, Mieke Massink and Herbert Wiklicky
Source:
QAPL - Tenth Workshop on Quantitative Aspects of Programming Languages. :63-76
Publisher Information:
CCSD; Open Publishing Association, 2012.
Publication Year:
2012
Collection:
collection:X
collection:CNRS
collection:INRIA
collection:LIX
collection:LIX-COMETE
collection:LIX-PARSIFAL
collection:INRIA-SACLAY
collection:X-DEP-INFO
collection:INRIA_TEST
collection:TESTALAIN1
collection:INRIA2
collection:INRIA-300009
Subject Terms:
robustness to errors., floating-point arithmetic, Program analysis, robustness to errors, ACM: F.: Theory of Computation, F.3: LOGICS AND MEANINGS OF PROGRAMS, F.3.1: Specifying and Verifying and Reasoning about Programs, [INFO.INFO-PL]Computer Science [cs], Programming Languages [cs.PL], [INFO.INFO-LO]Computer Science [cs], Logic in Computer Science [cs.LO]
Subject Geographic:
Tallinn, Estonia
Original Identifier:
ARXIV: 1202.0693
HAL: hal-00665995
Document Type:
Konferenz conferenceObject<br />Conference papers
Language:
English
Relation:
info:eu-repo/semantics/altIdentifier/arxiv/1202.0693; info:eu-repo/semantics/altIdentifier/doi/10.4204/EPTCS.85.5
DOI:
10.4204/EPTCS.85.5
Access URL:
https://inria.hal.science/hal-00665995
https://inria.hal.science/hal-00665995v3/document
https://inria.hal.science/hal-00665995v3/file/proof_example.pdf
Rights:
info:eu-repo/semantics/OpenAccess
Accession Number:
edshal.hal.00665995v3
Database:
HAL

Weitere Informationen

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.