Robustness Analysis of Floating-Point Programs by Self-Composition
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 prog...
Saved in:
| Main Authors: | , , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Wiley
2014-01-01
|
| Series: | Journal of Applied Mathematics |
| Online Access: | http://dx.doi.org/10.1155/2014/789213 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Summary: | 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. |
|---|---|
| ISSN: | 1110-757X 1687-0042 |