Paper Info
Title
Verifying floating-point programs with constraint programming and abstract interpretation techniques
Abstract
Static value analysis is a classical approach for verifying programs with floating-point computations. Value analysis mainly relies on abstract interpretation and over-approximates the possible values of program variables. State-of-the-art tools may however compute over-approximations that can be rather coarse for some very usual program expressions. In this paper, we show that constraint solvers can significantly refine approximations computed with abstract interpretation tools. More precisely, we introduce a hybrid approach combining abstract interpretation and constraint programming techniques in a single static and automatic analysis. This hybrid approach benefits from the strong points of abstract interpretation and constraint programming techniques, and thus, it is more effective than static analysers and constraint solvers, when used separately. We compared the efficiency of the system we developed--named rAiCp--with state-of-the-art static analyzers: rAiCp produces substantially more precise approximations and is able to check program properties on both academic and industrial benchmarks.
Year
DOI
Venue
2016
10.1007/s10515-014-0154-2
Automated Software Engineering
Keywords
Field
DocType
Program verification,Floating-point computation,Constraint solving over floating-point numbers,Constraint solving over real number intervals,Abstract interpretation-based approximation
Constraint satisfaction,Mathematical optimization,Expression (mathematics),Computer science,Floating point,Abstract interpretation,Constraint programming,Algorithm,Theoretical computer science,Constraint logic programming,Binary constraint,Computation
Journal
Volume
Issue
ISSN
23
2
0928-8910
Citations 
PageRank 
References 
7
0.48
25
Authors
3
Name
Order
Citations
PageRank
Olivier Ponsini1464.49
Claude Michel210710.57
Michel Rueher361359.81