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

Fingerprint

Static analysis
Costs
Experiments

Keywords

  • abstract interpretation
  • static program analyzers
  • widening

ASJC Scopus subject areas

  • Software

Cite this

Widening with thresholds via binary search. / Kim, Sol; Heo, Kihong; Oh, Hakjoo; Yi, Kwangkeun.

In: Software - Practice and Experience, Vol. 46, No. 10, 01.10.2016, p. 1317-1328.

Research output: Contribution to journalArticle

Kim, Sol ; Heo, Kihong ; Oh, Hakjoo ; Yi, Kwangkeun. / Widening with thresholds via binary search. In: Software - Practice and Experience. 2016 ; Vol. 46, No. 10. pp. 1317-1328.
@article{2c912ba76f5d4b7db22fe9fd140bab74,
title = "Widening with thresholds via binary search",
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.",
keywords = "abstract interpretation, static program analyzers, widening",
author = "Sol Kim and Kihong Heo and Hakjoo Oh and Kwangkeun Yi",
year = "2016",
month = "10",
day = "1",
doi = "10.1002/spe.2381",
language = "English",
volume = "46",
pages = "1317--1328",
journal = "Software - Practice and Experience",
issn = "0038-0644",
publisher = "John Wiley and Sons Ltd",
number = "10",

}

TY - JOUR

T1 - Widening with thresholds via binary search

AU - Kim, Sol

AU - Heo, Kihong

AU - Oh, Hakjoo

AU - Yi, Kwangkeun

PY - 2016/10/1

Y1 - 2016/10/1

N2 - 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.

AB - 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.

KW - abstract interpretation

KW - static program analyzers

KW - widening

UR - http://www.scopus.com/inward/record.url?scp=84986004490&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84986004490&partnerID=8YFLogxK

U2 - 10.1002/spe.2381

DO - 10.1002/spe.2381

M3 - Article

AN - SCOPUS:84986004490

VL - 46

SP - 1317

EP - 1328

JO - Software - Practice and Experience

JF - Software - Practice and Experience

SN - 0038-0644

IS - 10

ER -