Please use this identifier to cite or link to this item:
https://doi.org/10.1007/978-3-540-77505-8_26
Title: | Inferring disjunctive postconditions | Authors: | Popeea, C. Chin, W.-N. |
Issue Date: | 2007 | Citation: | Popeea, C.,Chin, W.-N. (2007). Inferring disjunctive postconditions. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 4435 LNCS : 331-345. ScholarBank@NUS Repository. https://doi.org/10.1007/978-3-540-77505-8_26 | Abstract: | Polyhedral analysis [9] is an abstract interpretation used for automatic discovery of invariant linear inequalities among numerical variables of a 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. © 2008 Springer-Verlag Berlin Heidelberg. | Source Title: | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) | URI: | http://scholarbank.nus.edu.sg/handle/10635/41039 | ISBN: | 3540775048 | ISSN: | 03029743 | DOI: | 10.1007/978-3-540-77505-8_26 |
Appears in Collections: | Staff Publications |
Show full item record
Files in This Item:
There are no files associated with this item.
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.