Abstract:

Polyhedral analysis is an abstract interpretation used for automatic discovery of invariant linear inequalities among numerical vari- ables of a program. Convexity of this abstract domain allows e±cient analysis but also loses precision via convex-hull and widening operators. To selectively recover the loss of precision, sets of polyhedra (disjunctive elements) may be used to capture more precise invariants. However a balance must be struck between precision and cost. We introduce the notion of a±nity to characterize how closely related is a pair of polyhedra. Finding related elements in the polyhedron (base) domain allows the formulation of precise hull and widening operators lifted to the disjunctive (powerset extension of the) polyhedron domain. We have implemented a modular static analyzer based on the disjunc- tive polyhedral analysis where the relational domain and the proposed operators can progressively enhance precision at a reasonable cost.

Paper: