Abstract
In this paper, we present a useful technique for implementing practical static program analyzers that use widening. Our technique aims to improve the efficiency of the conventional widening-with-thresholds technique at a small precision compromise. In static analysis, widening is used to accelerate (or converge) fixed point iterations. Unfortunately, this acceleration often comes with a significant loss in analysis precision. A standard method to improve the precision is to apply the widening with a set of thresholds. However, this technique may significantly slow down the analysis, because in practice it is commonplace to use a large set of thresholds. In worst case, the technique increases the analysis cost by the size N of the threshold set. In this paper, we propose a technique to reduce the worst case by log N, by employing a binary search in the process of applying threshold values. We formalize the technique in the abstract interpretation framework and show that, by experiments with a realistic static analyzer for C, our technique considerably improves the efficiency (by 81.5%) of the existing method with a small compromise (20.9%) on the analysis precision.
Original language | English |
---|---|
Pages (from-to) | 1317-1328 |
Number of pages | 12 |
Journal | Software - Practice and Experience |
Volume | 46 |
Issue number | 10 |
DOIs | |
Publication status | Published - 2016 Oct 1 |
Bibliographical note
Publisher Copyright:Copyright © 2015 John Wiley & Sons, Ltd.
Keywords
- abstract interpretation
- static program analyzers
- widening
ASJC Scopus subject areas
- Software