Refining Abstract Interpretation Based Value Analysis with Constraint Programming Techniques

Abstract interpretation based value analysis is a classical approach for verifying programs with floating-point computations. However, state-of-the-art tools compute an over-approximation of the variable values that can be very coarse. In this paper, we show that constraint solvers can significantly refine the approximations computed with abstract interpretation tools. We introduce a hybrid approach that combines abstract interpretation and constraint programming techniques in a single static and automatic analysis. RAICP, the system we developed is substantially more precise than FLUCTUAT, a state-of-the-art static analyser. Moreover, it could eliminate 13 false alarms generated by FLUCTUAT on a standard set of benchmarks.