Inferring Disjunctive Postconditions

10 years 8 months ago
Inferring Disjunctive Postconditions
Polyhedral analysis [9] is an abstract interpretation used for automatic discovery of invariant linear inequalities among numerical varia program. Convexity of this abstract domain allows efficient 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 affinity 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 disjunctive polyhedral analysis where the relational domain and the proposed operators can progressively enhance precision at a reasonable cost.
Corneliu Popeea, Wei-Ngan Chin
Added 20 Aug 2010
Updated 20 Aug 2010
Type Conference
Year 2006
Authors Corneliu Popeea, Wei-Ngan Chin
Comments (0)