Paper Info
Title
Combining widening and acceleration in linear relation analysis
Abstract
Linear Relation Analysis [CH78, Hal79] is one of the first, but still one of the most powerful, abstract interpretations working in an infinite lattice. As such, it makes use of a widening operator to enforce the convergence of fixpoint computations. While the approximation due to widening can be arbitrarily refined by delaying the application of widening, the analysis quickly becomes too expensive with the increase of delay. Previous attempts at improving the precision of widening are not completely satisfactory, since none of them is guaranteed to improve the precision of the result, and they can nevertheless increase the cost of the analysis. In this paper, we investigate an improvement of Linear Relation Analysis consisting in computing, when possible, the exact (abstract) effect of a loop. This technique is fully compatible with the use of widening, and whenever it applies, it improves both the precision and the performance of the analysis.
Year
DOI
Venue
2006
10.1007/11823230_10
SAS
Keywords
Field
DocType
widening operator,linear relation analysis,infinite lattice,abstract interpretation,fixpoint computation,combining widening,previous attempt
Convergence (routing),Computer science,Abstract interpretation,Static analysis,Convex hull,Algorithm,Operator (computer programming),Acceleration,Fixed point,Computation
Conference
Volume
ISSN
ISBN
4134
0302-9743
3-540-37756-5
Citations 
PageRank 
References 
50
1.52
19
Authors
2
Name
Order
Citations
PageRank
Laure Gonnord121111.01
Nicolas Halbwachs23957426.43