Parf: Adaptive Parameter Refining for Abstract Interpretation
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866912019151585280 |
|---|---|
| author | Wang, Zhongyi Yang, Linyu Chen, Mingshuai Bu, Yixuan Li, Zhiyang Wang, Qiuye Qin, Shengchao Yi, Xiao Yin, Jianwei |
| author_facet | Wang, Zhongyi Yang, Linyu Chen, Mingshuai Bu, Yixuan Li, Zhiyang Wang, Qiuye Qin, Shengchao Yi, Xiao Yin, Jianwei |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2409_05794 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Parf: Adaptive Parameter Refining for Abstract Interpretation Wang, Zhongyi Yang, Linyu Chen, Mingshuai Bu, Yixuan Li, Zhiyang Wang, Qiuye Qin, Shengchao Yi, Xiao Yin, Jianwei Logic in Computer Science D.2.4 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. |
| title | Parf: Adaptive Parameter Refining for Abstract Interpretation |
| topic | Logic in Computer Science D.2.4 |
| url | https://arxiv.org/abs/2409.05794 |