Papers › On Benchmarking the Capability of Symbolic Execution Tools with Logic Bombs
On Benchmarking the Capability of Symbolic Execution Tools with Logic Bombs
Hui Xu, Zirui Zhao, Yangfan Zhou, Michael R. Lyu
The archive published only this paper's code-link row. Authors, date and abstract are from arXiv's metadata (CC0), read from the Kaggle arXiv metadata snapshot of 2026-09-12 where its title matched the archive's; the title is the archive's.
Symbolic execution now becomes an indispensable technique for software testing and program analysis. There are several symbolic execution tools available off-the-shelf, and we need a practical benchmark approach to learn their capabilities. Therefore, this paper introduces a novel approach to benchmark symbolic execution tools in a fine-grained and efficient manner. In particular, our approach evaluates the performance of such tools against the known challenges faced by general symbolic execution techniques, such as floating-point numbers and symbolic memories. To this end, we first survey related papers and systematize the challenges of symbolic execution. We extract 12 distinct challenges from the literature and categorize them into two categories: symbolic-reasoning challenges and path-explosion challenges. Then, we develop a dataset of logic bombs and a framework to benchmark symbolic execution tools automatically. For each challenge, our dataset contains several logic bombs, each of which is guarded by a specific challenging problem. If a symbolic execution tool can find test cases to trigger logic bombs, it indicates that the tool can handle the corresponding problems. We have conducted real-world experiments with three popular symbolic execution tools: KLEE, Angr, and Triton. Experimental results show that our approach can reveal their capabilities and limitations in handling particular issues accurately and efficiently. The benchmark process generally takes only dozens of minutes to evaluate a tool. We release our dataset on GitHub as open source, with an aim to better facilitate the community to conduct future work on benchmarking symbolic execution tools.
Code
Repository list and official/mentioned flags are the archive's, frozen 2025-07-28. Reachability, where shown, is from one Syntology probe window (2026-09-16 to 2026-09-18); repositories not probed show nothing. GitHub stars are not tracked.
Code Syntology ran Syntology
Not run by Syntology. Nothing on this page verifies that the listed code works.
Datasets
Introduced by this paper, per the archive.
Results from the paper archive 2025-07-28
No leaderboard rows for this paper in the archive.
Report a problem or propose a change · a person checks every report against the paper or source before anything changes; decisions are listed on /corrections