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. © 2012 Springer-Verlag.
CITATION STYLE
Ponsini, O., Michel, C., & Rueher, M. (2012). Refining abstract interpretation based value analysis with constraint programming techniques. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7514 LNCS, pp. 593–607). https://doi.org/10.1007/978-3-642-33558-7_43
Mendeley helps you to discover research relevant for your work.