Solving constraints over the floating point numbers is a key issue in the process of software validation and verification. Techniques to solve such constraints on the basis of projection functions have been successfully developed. However, though correct, this approach can lead to slow convergence phenomena for very common constraints like addition and subtraction constraints. In this paper, we introduce new addition and subtraction constraints which, thanks to a new floating point subtraction property, directly compute optimal bounds for the domain of the variables at a low cost. Preliminary experiments have shown that these constraints can drastically speed up the filtering process.
Bitte loggen Sie sich ein, um Zugang zu diesem Inhalt zu erhalten
