Widening with thresholds via binary search

Sol Kim, Kihong Heo, Hakjoo Oh, Kwangkeun Yi

Research output: Contribution to journalArticle

1 Citation (Scopus)

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 languageEnglish
Pages (from-to)1317-1328
Number of pages12
JournalSoftware - Practice and Experience
Volume46
Issue number10
DOIs
Publication statusPublished - 2016 Oct 1

Keywords

  • abstract interpretation
  • static program analyzers
  • widening

ASJC Scopus subject areas

  • Software

Fingerprint Dive into the research topics of 'Widening with thresholds via binary search'. Together they form a unique fingerprint.

  • Cite this