一句话：提出全自动框架 Parf，将静态分析器外部参数建模为随机变量并增量精化，在时间预算内显著降低误报。
抽象解释是程序静态分析的核心形式化方法，但其效果高度依赖静态分析工具的大量外部参数（抽象域、分析策略等）配置：既要保持低误报率（精度）又要保证分析效率，调参长期依赖专家知识，难以自动化。本文提出全自动框架 Parf，将各类外部参数建模为定义在格化参数空间上的概率分布下的随机变量，通过反复“采样—分析”并累积中间结果，增量地精化这些概率分布，从而在给定时间预算内收敛到一组高精度的参数配置。作者在开源 C 程序静态分析器 Frama-C/Eva 之上实现了 Parf，并在 Frama-C OSCS 基准上与专家精化策略及 Frama-C/Eva 官方配置进行对比：Parf 在 34/37（91.9%）的程序仓库上取得最少误报数，其中 12/37（32.4%）为唯一最优；在复杂、大规模真实程序上亦表现出良好性能。
Abstract interpretation is a key formal method for the static analysis of programs. The core challenge in applying abstract interpretation lies in the configuration of abstraction and analysis strategies encoded by a large number of external parameters of static analysis tools. To attain low false-positive rates (i.e., accuracy) while preserving analysis efficiency, tuning the parameters heavily relies on expert knowledge and is thus difficult to automate. In this paper, we present a fully automated framework called Parf to adaptively tune the external parameters of abstract interpretation-based static analyzers. Parf models various types of parameters 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 parameter settings within a given time budget. We have implemented Parf on top of Frama-C/Eva - an off-the-shelf open-source static analyzer for C programs - and compared it against the expert refinement strategy and Frama-C/Eva's official configurations over the Frama-C OSCS benchmark. Experimental results indicate that Parf achieves the lowest number of false positives on 34/37 (91.9%) program repositories with exclusively best results on 12/37 (32.4%) cases. In particular, Parf exhibits promising performance for analyzing complex, large-scale real-world programs.
@inproceedings{paperbot8421,
title = {Parf: Adaptive Parameter Refining for Abstract Interpretation},
author = {Zhongyi Wang and Linyu Yang and Mingshuai Chen and Yixuan Bu and Zhiyang Li and Qiuye Wang and Shengchao Qin and Xiao Yi and Jianwei Yin},
booktitle = {ASE},
year = {2024},
doi = {10.1145/3691620.3695487}
}