Refining Abstract Interpretation-based Approximations with Constraint Solvers

Abstract. Programs with floating-point computations are tricky to de-velop because floating-point arithmetic differs from real arithmetic and has many counterintuitive properties. A classical approach to verify such programs consists in estimating the precision of floating-point computa-tions with respect to the same sequence of operations in an idealized interpretation—have been designed to address this problem. However, such tools compute an over-approximation of the domains of the vari-ables, both in the semantics of the floating-point numbers and in the se-mantics of the real numbers. This over-approximation can be very coarse on some programs. In this paper, we show that constraint solvers over floating-point numbers and real numbers can significantly refine the ap-proximations computed by Fluctuat. We managed to reduce drastically the domains of variables of C programs that are difficult to handle for abstract interpretation techniques implemented in Fluctuat. Key words: Program verification; Floating-point computation; C pro-grams; Abstract interpretation-based approximation; Interval-based con-straint solvers over real and floating-point numbers