Refining Abstract Interpretation-based Approximations with a Floating-point Constraint Solver

Abstract. Floating-point arithmetic differs from real arithmetic, which makes programming with floating-point numbers tricky. Estimating the precision of a floating-point computation in a program, i.e., estimat-ing the difference with the result of the same sequence of operations in an idealized real number semantics, is then necessary. Tools like Fluc-tuat, based on abstract interpretation, have been designed to address this problem. However, these tools compute an over-approximation of the domains of the floating-point variables that may be very coarse on some tricky programs. In this paper, we use a constraint solver over floating-point numbers to refine the over-approximation computed by Fluctuat and reduce the domains of floating-point variables. Our approach could be successfully applied to C programs that are difficult for abstract in-terpretation techniques as implemented in Fluctuat. Key words: Program verification; C programs; Abstract interpretation-based approximation; Floating-point computation; Floating-point con-straint solver