Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

PARF: An Adaptive Abstraction-Strategy Tuner for Static Analysis

Zhongyi Wang, Mingshuai Chen, Tengjie Lin, Linyu Yang, Junhao Zhuo, Qiuye Wang, Shengchao Qin, Xiao Yi, Jianwei Yin

TL;DR

Parf addresses the challenge of automatically tuning abstraction strategies in static analysis by modeling external parameters as probabilistic variables over latticed spaces and iteratively refining their distributions under a time budget. It introduces a compositional random-variable model with base and delta components to enable incremental knowledge retention and adaptive exploration, and it presents the Parf architecture with a web UI and distribution-refinement algorithms. Empirical results on OSCS benchmarks and SV-COMP tasks show Parf achieving state-of-the-art alarm reduction and verification improvements, along with insights into dominant parameters that drive accuracy-efficiency tradeoffs. The work advances practical static analysis by enabling scalable, automated configuration of analyzers like Frama-C/Eva and by providing interpretability through dominancy analyses and case studies.

Abstract

We launch Parf - a toolkit for adaptively tuning abstraction strategies of static program analyzers in a fully automated manner. Parf models various types of external parameters (encoding abstraction strategies) as random variables subject to probability distributions over latticed parameter spaces. It incrementally refines the probability distributions based on accumulated intermediate results generated by repeatedly sampling and analyzing, thereby ultimately yielding a set of highly accurate abstraction strategies. Parf is implemented on top of Frama-C/Eva - an off-the-shelf open-source static analyzer for C programs. Parf provides a web-based user interface facilitating the intuitive configuration of static analyzers and visualization of dynamic distribution refinement of the abstraction strategies. It further supports the identification of dominant parameters in Frama-C/Eva analysis. Benchmark experiments and a case study demonstrate the competitive performance of Parf for analyzing complex, large-scale real-world programs.

PARF: An Adaptive Abstraction-Strategy Tuner for Static Analysis

TL;DR

Parf addresses the challenge of automatically tuning abstraction strategies in static analysis by modeling external parameters as probabilistic variables over latticed spaces and iteratively refining their distributions under a time budget. It introduces a compositional random-variable model with base and delta components to enable incremental knowledge retention and adaptive exploration, and it presents the Parf architecture with a web UI and distribution-refinement algorithms. Empirical results on OSCS benchmarks and SV-COMP tasks show Parf achieving state-of-the-art alarm reduction and verification improvements, along with insights into dominant parameters that drive accuracy-efficiency tradeoffs. The work advances practical static analysis by enabling scalable, automated configuration of analyzers like Frama-C/Eva and by providing interpretability through dominancy analyses and case studies.

Abstract

We launch Parf - a toolkit for adaptively tuning abstraction strategies of static program analyzers in a fully automated manner. Parf models various types of external parameters (encoding abstraction strategies) as random variables subject to probability distributions over latticed parameter spaces. It incrementally refines the probability distributions based on accumulated intermediate results generated by repeatedly sampling and analyzing, thereby ultimately yielding a set of highly accurate abstraction strategies. Parf is implemented on top of Frama-C/Eva - an off-the-shelf open-source static analyzer for C programs. Parf provides a web-based user interface facilitating the intuitive configuration of static analyzers and visualization of dynamic distribution refinement of the abstraction strategies. It further supports the identification of dominant parameters in Frama-C/Eva analysis. Benchmark experiments and a case study demonstrate the competitive performance of Parf for analyzing complex, large-scale real-world programs.
Paper Structure (20 sections, 3 equations, 5 figures, 4 tables)

This paper contains 20 sections, 3 equations, 5 figures, 4 tables.

Table of Contents

  1. Introduction
  2. Problem and Methodology
  3. The P ARF Architecture
  4. Value-Space Encoding
  5. Parameter Sampling
  6. Program Analyzing
  7. Distribution Refining
  8. Empirical Evaluation
  9. Experimental Setup
  10. RQ1: Consistency
  11. RQ2: Verification Capability
  12. RQ3: Dominancy
  13. RQ4: Interpretability
  14. Limitations and Future Work
  15. Related Work
  16. ...and 5 more sections

Figures (5)

  • Figure 1: Architecture of the Parf artifact.
  • Figure 4: Fig. A1. Analysis results by selecting or excluding individual parameters on OSCS benchmarks.
  • Figure : Experimental Results in Terms of RQ1 (Consistency)
  • Figure : SV-COMP verification results in terms of RQ2 (Verification Capability)
  • Figure : Impact of Parameters in Terms of RQ3 (Dominancy)