Robustness analysis of finite precision implementations

Abstract : A desirable property of control systems is robustness to inputs, when small perturbations of the inputs of a system will cause only small perturbations on outputs. This property should be maintained at the implementation level, where close inputs can lead to different execution paths. The problem becomes crucial for finite precision implementations, where any elementary computation is affected by an error. In this context, almost every test is potentially unstable, that is, for a given input, the finite precision and real numbers paths may differ. Still, state-of-the-art error analyses rely on the stable test hypothesis, yielding unsound error bounds when the conditional block is not robust to uncertainties. We propose a new abstract-interpretation based error analysis of finite precision implementations, which is sound in presence of unstable tests, by bounding the discontinuity error for path divergences. This gives a tractable analysis implemented in the FLUCTUAT analyzer.
Document type :
Conference papers
Complete list of metadatas

https://hal-cea.archives-ouvertes.fr/cea-01834989
Contributor : Léna Le Roy <>
Submitted on : Wednesday, July 11, 2018 - 10:02:46 AM
Last modification on : Wednesday, January 23, 2019 - 2:39:33 PM

Links full text

Identifiers

Collections

CEA | DRT | LIST

Citation

E. Goubault, S. Putot. Robustness analysis of finite precision implementations. Programming Languages and Systems. APLAS 2013. Lecture Notes in Computer Science, Dec 2013, Melbourne, VIC, Australia. pp.50-57, ⟨10.1007/978-3-319-03542-0_4⟩. ⟨cea-01834989⟩

Share

Metrics

Record views

44