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.
Document type :
Conference papers
Static Analysis (SAS 2006), Aug 2006, Seoul, South Korea. pp.144-160, 2006, <10.1007/11823230_10>
Liste complète des métadonnées


https://hal.archives-ouvertes.fr/hal-00189614
Contributor : Nicolas Halbwachs <>
Submitted on : Wednesday, November 21, 2007 - 3:00:56 PM
Last modification on : Wednesday, November 21, 2007 - 9:48:23 PM
Document(s) archivé(s) le : Monday, April 12, 2010 - 3:06:32 AM

File

main.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Laure Gonnord, Nicolas Halbwachs. Combining Widening and Acceleration in Linear Relation Analysis. Static Analysis (SAS 2006), Aug 2006, Seoul, South Korea. pp.144-160, 2006, <10.1007/11823230_10>. <hal-00189614>

Share

Metrics

Record views

339

Document downloads

199