Widening with thresholds via binary search

Sol Kim, Kihong Heo, Hakjoo Oh, Kwangkeun Yi

    Research output: Contribution to journalArticlepeer-review

    3 Citations (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

    Bibliographical note

    Publisher Copyright:
    Copyright © 2015 John Wiley & Sons, Ltd.

    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