Widening with thresholds via binary search. (4th December 2015)

• Record Type: Journal Article
• Authors: Kim, Sol; Heo, Kihong; Oh, Hakjoo; Yi, Kwangkeun
• Is Part Of: Software, practice & experience. Volume 46:Number 10(2016)
• Page Start: 1317
• Page End: 1328
• Publication Date: 2015-12-04
• Subjects: static program analyzers -- abstract interpretation -- widening; Computer software -- Periodicals; Computer programming -- Periodicals; Computer programs -- Periodicals; 005.3
• DOI: 10.1002/spe.2381
• Languages: English
• ISSNs: 0038-0644

Abstract

Summary: 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. Copyright © 2015 John Wiley & Sons, Ltd.