Mixed Abstractions for Floating-Point Arithmetic

Publication Type:

Conference Paper

Source:

FMCAD, IEEE, p.69-76 (2009)

URL:

http://dx.doi.org/10.1109/FMCAD.2009.5351141

Abstract:

Floating-point arithmetic is essential for many embedded and safety-critical systems, such as in the avionics industry. Inaccuracies in floating-point calculations can cause subtle changes of the control flow, potentially leading to disastrous errors. In this paper, we present a simple and general, yet powerful framework for building abstractions from formulas, and instantiate this framework to a bit-accurate, sound and complete decision procedure for IEEE-compliant binary floating-point arithmetic. Our procedure benefits in practice from its ability to flexibly harness both over- and underapproximations in the abstraction process. We demonstrate the potency of the procedure for the formal analysis of floating-point software.