Precise Data-Driven Approximation for Program Analysis via Fuzzing
Nikhil Parasaram, Earl T. Barr, Sergey Mechtaev, Marcel Böhme
Abstract
Program analysis techniques such as abstract interpretation and symbolic execution suffer from imprecision due to over- and underapproximation, which results in false alarms and missed violations. To alleviate this imprecision, we propose a novel data structure, program state probability (PSP), that leverages execution samples to probabilistically approximate reachable program states. The core intuition of this approximation is that the probability of reaching a given state varies greatly, and thus we can considerably increase analysis precision at the cost of a small probability of unsoundness or incompleteness, which is acceptable when analysis targets bug-finding. Specifically, PSP enhances existing analyses by disregarding low-probability states deemed feasible by overapproximation and recognising high-probability states deemed infeasible by underapproximation. We apply PSP in three domains. First, we show that PSP enhances the precision of the Clam abstract interpreter in terms of MCC from 0.09 to 0.27 and F1 score from 0.22 to 0.34. Second, we demonstrate that a symbolic execution search strategy based on PSP that prioritises program states with a higher probability increases the number of found bugs and reduces the number of solver calls compared to state-of-the-art techniques. Third, a program repair patch prioritisation strategy based on PSP reduces the average patch rank by 26%.
Ask about this paper
Your agent reads all of it.
Lune indexed this paper to the last equation, along with the top-tier papers that cite it. Ask a question and the answer quotes them.
Your agent calls
Luneget_paper_fulltext
Free to start. No credit card required.
Terminal
Install the CLIlune papers fulltext c9bfa77a-440f-418c-a87f-ab6c65eebf57Cited by top-tier papers2
- Statistical Reachability AnalysisSeongmin Lee, Marcel BöhmeFSE 2023 · 12 citations
- Abstract Interpretation with Confidence: Quantifying the Precision of Dataflow Analysis with ProbabilitiesYuanfeng Shi, Ziyue Jin, Xin ZhangPLDI 2026
Builds on7
- Empirical review of automated analysis tools on 47, 587 Ethereum smart contractsThomas Durieux, João F. Ferreira, Rui Abreu, Pedro CruzICSE 2020 · 373 citations
- Finding real bugs in big programs with incorrectness logicQuang Loc Le, Azalea Raad, Jules Villard, Josh Berdine et al.OOPSLA 2022 · 52 citations
- Neuro-Symbolic Execution: Augmenting Symbolic Execution with Neural ConstraintsShiqi Shen, Shweta Shinde, Soundarya Ramesh, Abhik Roychoudhury et al.NDSS 2019 · 43 citations
- Statistical Reachability AnalysisSeongmin Lee, Marcel BöhmeFSE 2023 · 12 citations
- Rete: Learning Namespace Representation for Program RepairNikhil Parasaram, Earl T. Barr, Sergey MechtaevICSE 2023 · 12 citations
Related papers
- Empc: Effective Path Prioritization for Symbolic Execution with Path CoverShuangjie Yao, Dongdong SheS&P 2025
- PREACH: A Heuristic for Probabilistic Reachability to Identify Hard to Reach StatementsSeemanta Saha, Mara Downing, Tegan Brennan, Tevfik BultanICSE 2022 · 11 citations
- Learning to Explore Paths for Symbolic ExecutionJingxuan He, Gishor Sivanrupan, Petar Tsankov, Martin T. VechevCCS 2021 · 39 citations
- Доверя'й, но проверя'й: SFI safety for native-compiled WasmEvan Johnson, David Thien, Yousef Alhessi, Shravan Narayan et al.NDSS 2021
- Engineering a Formally Verified Automated Bug FinderArthur Correnson, Dominic SteinhöfelFSE 2023 · 6 citations
