Weakly-Relational Shapes for Numeric Abstractions: Improved Algorithms and Proofs of Correctness

Publication TypeJournal Article
Year of Publication2009
AuthorsBagnara R, Hill PM, Zaffanella E
JournalFormal Methods in System Design
Keywordsabstract interpretation, integer constraints, octagonal constraints, software verification, static analysis, unit two variables per inequality constraints, UTVPI constraints

Weakly-relational numeric constraints provide a compromise between complexity and expressivity that is adequate for several applications in the field of formal analysis and verification of software and hardware systems. We address the problems to be solved for the construction of full-fledged, efficient and provably correct abstract domains based on such constraints. We first propose to work with semantic abstract domains, whose elements are geometric shapes, instead of the (more concrete) syntactic abstract domains of constraint networks and matrices on which the previous proposals are based. This allows to solve, once and for all, the problem whereby closure by entailment, a crucial operation for the realization of such domains, seemed to impede the realization of proper widening operators. In our approach, the implementation of widenings relies on the availability of an effective reduction procedure for the considered constraint description: one for the domain of bounded difference shapes already exists in the literature; we provide algorithms for the significantly more complex cases of rational and integer octagonal shapes. We also improve upon the state-of-the-art by presenting, along with their proof of correctness, closure by entailment algorithms of reduced complexity for domains based on rational and integer octagonal constraints. The consequences of implementing weakly-relational numerical domains with floating point numbers are also discussed.

File attachments: 
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.