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
Source: 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.

SCOPUSTM   
Citations

23
checked on Dec 13, 2017

Page view(s)

34
checked on Dec 9, 2017

Google ScholarTM

Check

Altmetric


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.