Mixed abstractions for floating-point arithmetic

stractions for Floating-Point Arithmetic Angelo Brillout Computer Systems Institute, ETH Zurich Daniel Kroening and Thomas Wahl Oxford University Computing Laboratory 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 framework for building abstractions from formulas, and instantiate this framework to a bit-accurate, sound and complete decision procedure for IEEE-compliant binary floatingpoint arithmetic. Our procedure benefits in practice from its ability to flexibly harness both over- and underapproximations bstraction process. We demonstrate the potency of the procedure for the formal analysis of floating-point software.

• Type: Conference
• Year: 2009
• Where: FMCAD
• Authors: Angelo Brillout, Daniel Kroening, Thomas Wahl
• Keywords: Floating-Point Arithmetic Angelo, FMCAD 2009, Formal Methods, Laboratory Abstract—Floating-point Arithmetic, Zurich Daniel Kroening