Robustness Analysis of Floating-Point Programs by Self-Composition

Joint Authors

Yin, Banghu
Wang, Ji
Chen, Liqian
Dong, Wei
Jiang, Jiahong

Source

Journal of Applied Mathematics

Issue

Vol. 2014, Issue 2014 (31 Dec. 2014), pp.1-12, 12 p.

Publisher

Hindawi Publishing Corporation

Publication Date

2014-05-20

Country of Publication

Egypt

No. of Pages

12

Main Subjects

Mathematics

Abstract EN

Robustness is a key property for critical systems that run in uncertain environments, to ensure that small input perturbations can cause only small output changes.

Current critical systems often involve lots of floating-point computations which are inexact.

Robustness analysis of floating-point programs needs to consider both the uncertain inputs and the inexact computation.

In this paper, we propose to leverage the idea of self-composition to transform the robustness analysis problem into a reachability problem, which enables the use of standard reachability analysis techniques such as software model checking and symbolic execution for robustness analysis.

To handle floating-point arithmetic, we employ an abstraction that encompasses the effect of rounding and that can encompass all rounding modes.

It converts floating-point expressions into linear expressions with interval coefficients in exact real arithmetic.

On this basis, we employ interval linear programming to compute the maximum output change or maximum allowed input perturbation for the abstracted programs.

Preliminary experimental results of our prototype implementation are encouraging.

American Psychological Association (APA)

Chen, Liqian& Jiang, Jiahong& Yin, Banghu& Dong, Wei& Wang, Ji. 2014. Robustness Analysis of Floating-Point Programs by Self-Composition. Journal of Applied Mathematics،Vol. 2014, no. 2014, pp.1-12.
https://search.emarefa.net/detail/BIM-498165

Modern Language Association (MLA)

Chen, Liqian…[et al.]. Robustness Analysis of Floating-Point Programs by Self-Composition. Journal of Applied Mathematics No. 2014 (2014), pp.1-12.
https://search.emarefa.net/detail/BIM-498165

American Medical Association (AMA)

Chen, Liqian& Jiang, Jiahong& Yin, Banghu& Dong, Wei& Wang, Ji. Robustness Analysis of Floating-Point Programs by Self-Composition. Journal of Applied Mathematics. 2014. Vol. 2014, no. 2014, pp.1-12.
https://search.emarefa.net/detail/BIM-498165

Data Type

Journal Articles

Language

English

Notes

Includes bibliographical references

Record ID

BIM-498165