New paper on widenings for weakly-relational numeric abstractions

Wed, 04/13/2005 - 19:51

Widening Operators for Weakly-Relational Numeric Abstractions presents the solution to the problem of defining proper widening operators on several weakly-relational numeric abstractions (including bounded differences and octagons). The proposed solution has the big advantage of allowing the adoption of the semantic versions of the abstract domains, whose elements are geometric shapes, instead of the syntactic domains of constraint networks and matrices (which are more difficult to use and to integrate into analysis tools). The implementation of the proposed widenings relies on the availability of an effective reduction procedure for the considered constraint description: the paper provides such an algorithm for the domain of octagonal shapes. As a bonus, the paper also presents an improvement of the strong closure algorithm defined in Min01a that is worth a reduction of the number of additions and comparisons in the range 15-20%, for octagons of dimension greater than 4.
The presented algorithms are already part of the implementation of bounded differences and octagons that will be included in future releases of the PPL.

We are a passionate team of experts. Do not hesitate to let us have your feedback:
You may be surprised to discover just how much your suggestions matter to us.