Pith. sign in

REVIEW 4 major objections 6 minor 91 references

LLM-marked source locations plus loop-exit prioritization steer symbolic execution to more security violations than existing exploration strategies can find.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

T0 review · deepseek-v4-flash

2026-08-01 08:15 UTC pith:T6QJTDCM

load-bearing objection Solid empirical LLM-guided symbolic execution paper with a real new combination and a strong replication package; the unique-violation margin over random-path is narrow and the leakage control is partial. the 4 major comments →

arxiv 2607.21676 v1 pith:T6QJTDCM submitted 2026-07-23 cs.SE

Directed Symbolic Execution for Vulnerability Discovery: An LLM-Guided Approach in KLEE

Lingfeng Chen , Tao Xiao , Masanari Kondo , Yasutaka Kamei This is my paper
classification cs.SE
keywords symbolic executionpath explosionpath prioritizationLLMKLEEdirected symbolic executionsecurity violation discoveryloop-exit prioritization
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

This paper tries to show that a symbolic-execution engine can find more security violations if an LLM first marks the code locations most likely to be vulnerable, and if the engine also avoids getting trapped in loops that contain no such marked locations. The proposed system, KLEECopilot, steers path prioritization toward these LLM-generated markings and away from unmarked cyclic regions. On 11 real-world programs, it reports 1,335 total and 87 unique sanitizer-confirmed violations, beating the second-best of 13 existing strategies by 32.2% and 7.4%, and on 12 programs it reports 125.82% higher line coverage and 42.24% higher basic-block coverage than the strongest prior path-prioritization baseline. The results matter because path explosion is the main bottleneck in symbolic execution, and this is a way to spend the exploration budget where vulnerabilities actually are. A sympathetic reader would take this as evidence that LLM semantic knowledge can substitute for hand-written rules in directing program exploration.

Core claim

The central claim is that path prioritization in symbolic execution can be guided by semantic, LLM-derived markings of potentially vulnerable code rather than by coverage-oriented structural heuristics, and that this guidance becomes materially more effective when combined with a loop-exit rule: cyclic regions that contain no marking are treated as traps and the searcher prefers leaving them, while marked cyclic regions continue to be explored. On the paper's benchmarks, KLEECopilot finds 1,335 total violations and 87 unique violations, versus 1,010 and 81 for the second-best baseline, and it reports that removing either component lowers unique violations to roughly 54–61. The paper also rep

What carries the argument

The mechanism is a custom searcher inside KLEE driven by two inputs. First, an LLM produces line-level markings of potentially vulnerable code from preprocessed source, using a prompt that defines integer-overflow and memory-safety violation types. Second, an interprocedural control-flow graph is built, strongly connected components are collapsed to identify cyclic regions, and each region is classified by whether it contains any marking. The searcher then applies four ordered criteria: shortest graph distance to the nearest marking (markings are consumed once reached), exit from unmarked cyclic regions, greater basic-block depth, and random selection after a 35-million-instruction coverage

Load-bearing premise

The load-bearing premise is that the LLM's markings reflect genuine security semantics rather than memorized knowledge of these particular benchmark programs; if the model is instead recalling vulnerabilities it saw in training, the measured advantage over the baselines would not transfer to unseen code.

What would settle it

Run KLEECopilot on C/C++ programs written entirely after the marking model's training cutoff, or on the existing 12 benchmarks after removing or renaming any code the model could have memorized, and compare violation counts with the reported 87 unique violations. If the advantage disappears on genuinely unseen code, the head-line result was carried by training-data leakage, not by the prioritization mechanism. A weaker test: give the marking model only function signatures, without the bodies, and see whether it can reproduce the exact vulnerable line numbers of the 12 benchmarks at rates far a

Watch this falsifier — get emailed when new claim-graph text bears on it.

If this is right

  • Symbolic-execution engines can treat LLM-generated source markings as a practical source of vulnerability-oriented targets, covering a broader range of bug types than hand-written static-analysis rules.
  • A 10-hour run with this guidance finds roughly a third more total violations and 7% more distinct bug types than the best existing strategy on the same benchmark suite, and substantially more than graph-coverage-driven prioritization.
  • The ablation results imply that neither LLM guidance alone nor loop-exit prioritization alone explains the gain: removing either drops unique violations from 87 to 61 or 58.
  • Higher code coverage does not automatically mean better violation discovery, since a variant with higher coverage found fewer unique violations; evaluations of such tools should measure violations directly.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Beyond the paper: a natural extension is to feed KLEE's solver results and coverage feedback back into the marking step, so markings the engine cannot reach are revised instead of consuming budget; the paper itself leaves reachability as future work.
  • Beyond the paper: the loop-exit rule has a trade-off the authors acknowledge in passing — a vulnerability inside a loop that the LLM fails to mark will be actively deprioritized, so combining the searcher with a loop-aware fallback would be a worthwhile stress test.
  • Beyond the paper: the result that model family matters more than scale suggests future work should identify which training properties produce useful vulnerability markings, rather than simply scaling up models.
  • Beyond the paper: if the leakage risk is low, the marking step is cheap enough to serve as a pre-filter before deeper fuzzing or static analysis; the expensive 10-hour symbolic run is the part that would need scheduling.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Referee Report

4 major / 6 minor

Summary. KLEECopilot is an LLM-guided directed symbolic execution approach built on KLEE. It uses LLM-generated line-level markings of potentially vulnerable code to compute ICFG distances, and adds loop-exit prioritization based on SCC collapse to avoid spending budget in unmarked cyclic regions. A custom searcher (C1–C4) combines these signals. The evaluation uses the 12 Empc benchmark programs, 13 baselines, 7 LLMs, and 4 ablation groups, with five repeated 10-hour runs per configuration. The paper claims that KLEECopilot achieves the best security violation discovery (1,335 total, 87 unique; vs. 1,010/81 for random-path and 721/70 for Empc), large coverage improvements over Empc (125.82% line, 42.24% basic-block), and that both LLM-guided prioritization and loop-exit prioritization are necessary, because ablations find only 54–61 unique violations.

Significance. If the central comparative claim is valid, the paper makes a useful contribution: it is the first to show that LLM security semantics can be operationalized as source-level markings that guide KLEE's search, and it combines this with a principled loop-exit mechanism. The empirical infrastructure is a strength: 13 baselines, multiple LLM families and sizes, a full ablation design, a Dockerized replication package, and developer-confirmed newly reported violations. The paper is also careful in several places, e.g., macro preprocessing to align source and bitcode, and replay-based sanitizer validation. However, the headline result rests on two currently unsupported pillars: the 87-vs-81 unique-violation margin is reported only as point estimates without per-run variation, and the leakage analysis in §6.1 explicitly leaves 81.98% of LLM markings potentially derived from code seen during training. The significance is therefore conditional; the method may be genuinely effective, but the evaluation as written does not yet separate the proposed guidance mechanism from LLM memorization of well-known benchmark code.

major comments (4)
  1. [§6.1 / RQ2] The data-leakage mitigation is acknowledged by the paper itself to be incomplete. Section 6.1 states that only 18.02% of markings correspond to post-training-date lines, so 81.98% could involve code seen during training. The zenc check is not run under the RQ2 protocol: it reports only 'still outperforms most baselines' and gives no unique-violation counts, no per-benchmark breakdown, and no indication of the 5-run/10-hour protocol. Since the central RQ2 claim is a 6-unique-violation margin over random-path (87 vs. 81), this is load-bearing. Please add a strict post-training-cutoff evaluation using the same protocol, or otherwise provide per-benchmark unique violations on code provably after the training cutoff, and compare markings against a non-memorizing source on those benchmarks. The ablations in RQ4 reduce but do not eliminate this concern, because all variants use the same possibl
  2. [§5.3, Table 3] No per-run variance is reported for unique or total violations. The five runs are aggregated via a CASR-style dedup, but it is not stated whether the reported counts are the union across runs (as the description of 'across the five experiments' suggests). With union-based aggregation, a single unusually good run can create the reported 87, and the 7.4% margin over random-path may depend on that run. Please report the per-run distribution (min/median/max, and ideally all five runs) for KLEECopilot and the top baselines, and state explicitly whether deduplication is performed per run before aggregation or over the union of all runs. If union is used, also report the number of unique violations found in at least k of 5 runs.
  3. [§5.2, Figure 5 and RQ1 conclusion] The abstract and RQ1 conclusion state that KLEECopilot improves basic-block coverage by 42.24% over Empc, but the paper's own text in §5.2 reports that KLEECopilot is worse in basic-block coverage on 5 of 12 benchmarks (transicc −37.61%, bison −22.33%, curl −10.92%, tiffinfo −10.88%, jasper −65.11%). The aggregate improvement is therefore driven by a few large wins and does not justify the unqualified statement that KLEECopilot 'outperformed other baselines' in coverage. Please report per-benchmark deltas and interpret the mixed basic-block pattern explicitly, both in the RQ1 conclusion and in the abstract.
  4. [§4.3 (C4) and §5.5 (Random markings)] Two design decisions are hand-set free parameters with no sensitivity analysis: the 35M-instruction coverage-stall threshold in C4, and the random-marking density in RQ4 (matched to the 8.03% average function-level marking ratio of four local LLMs). The claims in RQ4 ('random markings discover 61 vs. 87') depend on this particular density. Please add a small sensitivity analysis for these parameters, or at minimum state explicitly that the conclusions are conditional on them. This is not a claim of circularity, but a request for evidence that the central results do not hinge on the chosen values.
minor comments (6)
  1. [§6.1] The zenc experiment is described qualitatively. Please provide the project's size, the number of markings used, the number of violations found by KLEECopilot and by each baseline, and the coverage numbers, so that the reader can judge whether 'outperforms most baselines' is statistically or practically meaningful.
  2. [§5.3 / §5.4] The text in §7 says results are reported as 'mean with one standard deviation,' but Tables 3–5 and the RQ2/RQ3 text do not give standard deviations or confidence intervals for violation counts. Please make the variance reporting consistent across RQs.
  3. [Table 4 and Table 5] The random-path row is based on 10 benchmarks while other rows use 12 (due to state exhaustion in jasper and readelf). Comparing median deltas across rows with different benchmark sets is potentially misleading; please mark this clearly in the table or repeat the comparison on the common 10-benchmark subset.
  4. [Figure 6] The Venn diagram numbers are difficult to read and the diagram does not show which benchmark each exclusive violation belongs to. A table listing the exclusive violations per strategy and benchmark would be more informative.
  5. [Page 1 and 27] The ACM reference format line says 'July 2018' and the Received/date block says 'Received 20 February 2007; revised 12 March 2009; accepted 5 June 2009,' which are clearly template leftovers. Please correct the publication date metadata.
  6. [§4.3] C4 says the searcher returns to random after 35M instructions 'without covering any new basic block.' Please define the scope of 'new' (per run, per searcher instance) and state whether this is measured on the whole program or on the current region.

Circularity Check

0 steps flagged

No significant circularity: violation discovery is independently replayed and sanitizer-confirmed; LLM markings are input guidance, not fitted outputs.

full rationale

KLEECopilot's derivation chain is a pipeline: (i) LLM prompts with CWE/sanitizer definitions produce line-level markings (Section 4.1); (ii) markings are mapped to ICFG nodes and BFS distances are computed (Section 4.2); (iii) a hand-designed searcher prioritizes by distance, loop-exit, depth, and a 35M-instruction fallback (Section 4.3). Nothing in this chain estimates or fits the RQ2 violation counts; those counts are produced by running KLEE under a 10-hour budget, replaying generated tests on ASan/UBSan binaries, and deduplicating with CASR (Section 5.3). The central claim is therefore not equivalent to its inputs by construction: the ablation study shows that the same LLM markings yield only 54 unique violations with SDSE, 61 with v1, 58 with v2, and 61 with random markings, so the searcher and loop-exit components add independent content. No self-citation is load-bearing; reference [22] is only the replication package, and all baselines (Empc, SDSE, etc.) are external prior work. The paper's own leakage limitation (Sections 6.1 and 7) is a genuine threat to external validity: 81.98% of markings could correspond to code the LLM saw in training, and only one post-cutoff project is tested. But data leakage is a possible confound, not a circular reduction: even a memorized marking is an input to KLEE, not a quantity derived from the paper's reported outcomes, and the paper does measure 18.02% of markings on post-training lines. Because no equation-level, definitional, or self-citation reduction can be exhibited, the appropriate finding is no significant circularity (score 0).

Axiom & Free-Parameter Ledger

2 free parameters · 5 axioms · 0 invented entities

The method's central mechanism adds no fitted constants to KLEE; the only hand-set numeric parameter is the 35M-instruction fallback threshold. The real burden is carried by domain assumptions about LLM marking quality, ICFG-distance guidance, and sanitizer replay validity.

free parameters (2)
  • C4 coverage-stall threshold = 35 million instructions
    Set in §4.3 based on preliminary experiments; hand-chosen fallback threshold for switching to random selection when no new basic block is covered. Not fitted to target violations, but a free design parameter.
  • Random-marking ablation density = 8.03% average function-level marking ratio
    In §5.5, random markings are generated to match the average marking ratio of four local LLMs; used only for the ablation control, not in KLEECopilot itself.
axioms (5)
  • standard math Tarjan's SCC algorithm on the ICFG correctly identifies all cyclic control-flow regions, including inter-procedural recursion.
    Invoked in §4.2 to classify loops; Tarjan's algorithm is standard, but the ICFG construction from LLVM bitcode and debug metadata is an engineering assumption.
  • domain assumption The LLM's markings are semantically relevant to real security violations rather than memorized benchmark answers.
    Core premise of the method; supported only empirically (§5.4, §6.1), and leakage is only partially excluded.
  • domain assumption Replaying KLEE-generated tests on ASan/UBSan-instrumented binaries is a valid oracle for security violations.
    Used in RQ2; the paper acknowledges sanitizer replay can behave differently from normal execution and repeats replays five times.
  • domain assumption Macro-expansion via the same compiler environment makes LLM-marked source lines correspond to the LLVM bitcode KLEE explores.
    Stated in §4.1 and Figure 2; needed for line-level markings to map to ICFG nodes.
  • domain assumption BFS distance on a unit-weight ICFG is a useful proxy for exploration progress toward markings.
    Used in §4.2 C1; no evidence that shortest-path distance correlates with symbolic feasibility under path constraints.

pith-pipeline@v1.3.0-alltime-deepseek · 28906 in / 14317 out tokens · 137964 ms · 2026-08-01T08:15:20.250347+00:00 · methodology

0 comments
read the original abstract

Symbolic execution effectively discovers security violations but suffers from path explosion. Engines like KLEE therefore use path prioritization heuristics to order state exploration, typically optimizing code coverage. However, path prioritization can become trapped in cyclic control-flow regions, where repeated branching consumes the exploration budget before exploration reaches vulnerable code beyond these cyclic regions. We propose KLEECopilot, a Large Language Model (LLM)-guided directed symbolic execution approach built on KLEE. KLEECopilot uses LLMs to mark potentially vulnerable code and guide path prioritization. It also integrates loop-exit prioritization to escape potentially non-vulnerable cycles and progress toward deeper vulnerabilities. Compared with baselines such as Empc, KLEECopilot improves basic block coverage by 42.24% and line coverage by 125.82%. It discovers 1,335 total violations and 87 unique violations, outperforming the second-best baseline by 32.2% in total violations and Empc by 24.3% in unique violations. Although KLEECopilot is sensitive to model family, it exhibits only marginal sensitivity to model scale, supporting the efficacy of integrating security semantics and loop-exit prioritization. Ablation studies further show that individual components contribute to effectiveness: alternative configurations involving searchers, internal components, marking sources, and prompt variants yield only 54--61 unique violations, while KLEECopilot maintains competitive code coverage.

Figures

Figures reproduced from arXiv: 2607.21676 by Lingfeng Chen, Masanari Kondo, Tao Xiao, Yasutaka Kamei.

Figure 1
Figure 1. Figure 1: Motivation and overview of KLEECopilot. (a) Path explosion in symbolic execution: repeated loop branching quickly increases the number of KLEE states, while the vulnerability-reaching execution may require selecting the appropriate loop body or loop-exit path. (b) Overall architecture of KLEECopilot, which generates LLM-based markings from benchmark code and uses them to guide distance computation and stat… view at source ↗
Figure 2
Figure 2. Figure 2: After pre-processing, the source code is macro-free, which is consistent with the LLVM bitcode binary [PITH_FULL_IMAGE:figures/full_fig_p006_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Prompt template and response for identifying potentially vulnerable locations within a given program [PITH_FULL_IMAGE:figures/full_fig_p007_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Line coverage over time during ten hours of symbolic exploration [PITH_FULL_IMAGE:figures/full_fig_p011_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Basic-block coverage over time during ten hours of symbolic exploration [PITH_FULL_IMAGE:figures/full_fig_p012_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Venn diagrams of unique violations discovered by the top-5 ranking strategies [PITH_FULL_IMAGE:figures/full_fig_p014_6.png] view at source ↗

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

91 extracted references · 14 canonical work pages

  1. [1]

    Md Basim Uddin Ahmed, Nima Shiri Harzevili, Jiho Shin, Hung Viet Pham, and Song Wang. 2026. SecVulEval: Context- Aware Benchmarking of LLMs for Vulnerability Detection. InProceedings of the 3rd ACM International Conference on AI-Powered Software(Montreal, QC, Canada)(AIware ’26). Association for Computing Machinery, New York, NY, USA, 388–396. doi:10.1145...

    arXiv 2026

  2. [2]

    Thanassis Avgerinos, Alexandre Rebert, Sang Kil Cha, and David Brumley. 2014. Enhancing symbolic execution with veritesting. InProceedings of the 36th International Conference on Software Engineering(Hyderabad, India)(ICSE 2014). Association for Computing Machinery, New York, NY, USA, 1083–1094. doi:10.1145/2568225.2568293

    arXiv 2014

  3. [3]

    Domagoj Babić, Lorenzo Martignoni, Stephen McCamant, and Dawn Song. 2011. Statically-directed dynamic automated test generation. InProceedings of the 2011 International Symposium on Software Testing and Analysis(Toronto, Ontario, Canada)(ISSTA ’11). Association for Computing Machinery, New York, NY, USA, 12–22. doi:10.1145/2001420.2001423 ACM Trans. Softw...

    arXiv 2011

  4. [4]

    Jaehyeon Bae, Seoryeong Kwon, and Seunghwan Myeong. 2024. Enhancing Software Code Vulnerability Detection Using GPT-4o and Claude-3.5 Sonnet: A Study on Prompt Engineering Techniques.Electronics13, 13 (2024). doi:10. 3390/electronics13132657

    2024

  5. [5]

    Roberto Baldoni, Emilio Coppa, Daniele Cono D’elia, Camil Demetrescu, and Irene Finocchi. 2018. A Survey of Symbolic Execution Techniques.ACM Comput. Surv.51, 3, Article 50 (May 2018), 39 pages. doi:10.1145/3182657

    doi:10.1145/3182657 2018

  6. [6]

    Al Bessey, Ken Block, Ben Chelf, Andy Chou, Bryan Fulton, Seth Hallem, Charles Henri-Gros, Asya Kamsky, Scott McPeak, and Dawson Engler. 2010. A few billion lines of code later: using static analysis to find bugs in the real world. Commun. ACM53, 2 (Feb. 2010), 66–75. doi:10.1145/1646353.1646374

    arXiv 2010

  7. [7]

    Marcel Böhme, Eric Bodden, Tevfik Bultan, Cristian Cadar, Yang Liu, and Giuseppe Scanniello. 2025. Software Security Analysis in 2030 and Beyond: A Research Roadmap.ACM Trans. Softw. Eng. Methodol.34, 5, Article 144 (May 2025), 26 pages. doi:10.1145/3708533

    doi:10.1145/3708533 2025

  8. [8]

    Marcel Böhme, Van-Thuan Pham, Manh-Dung Nguyen, and Abhik Roychoudhury. 2017. Directed Greybox Fuzzing. In Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security(Dallas, Texas, USA)(CCS ’17). Association for Computing Machinery, New York, NY, USA, 2329–2344. doi:10.1145/3133956.3134020

    arXiv 2017

  9. [9]

    Dimitrios Stamatios Bouras and Sergey Mechtaev. 2026. Gordian: Defusing Logic Bombs in Symbolic Execution with LLM-Generated Ghost Code. arXiv:2603.19239 [cs.SE] https://arxiv.org/abs/2603.19239

    arXiv 2026

  10. [10]

    Marc Bruni, Fabio Gabrielli, Mohammad Ghafari, and Martin Kropp. 2025. Benchmarking Prompt Engineering Techniques for Secure Code Generation with GPT Models. (2025), 93–103. doi:10.1109/Forge66646.2025.00018

    arXiv 2025

  11. [11]

    Suhabe Bugrara and Dawson Engler. 2013. Redundant state detection for dynamic symbolic execution. InProceedings of the 2013 USENIX Conference on Annual Technical Conference(San Jose, CA)(USENIX ATC’13). USENIX Association, USA, 199–212

    2013

  12. [12]

    Donaldson

    Frank Busse, Pritam Gharat, Cristian Cadar, and Alastair F. Donaldson. 2022. Combining static analysis error traces with dynamic symbolic execution (experience paper). InProceedings of the 31st ACM SIGSOFT International Symposium on Software Testing and Analysis(Virtual, South Korea)(ISSTA 2022). Association for Computing Machinery, New York, NY, USA, 568...

    arXiv 2022

  13. [13]

    Frank Busse, Martin Nowack, and Cristian Cadar. 2020. Running symbolic execution forever. InProceedings of the 29th ACM SIGSOFT International Symposium on Software Testing and Analysis(Virtual Event, USA)(ISSTA 2020). Association for Computing Machinery, New York, NY, USA, 63–74. doi:10.1145/3395363.3397360

    arXiv 2020

  14. [14]

    Frank Busse, Martin Nowack, and Cristian Cadar. 2024. Sparse Symbolic Loop Execution (Registered Report). InPro- ceedings of the 3rd ACM International Fuzzing Workshop(Vienna, Austria)(FUZZING 2024). Association for Computing Machinery, New York, NY, USA, 61–69. doi:10.1145/3678722.3685535

    arXiv 2024

  15. [15]

    Cristian Cadar, Daniel Dunbar, and Dawson Engler. 2008. KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. InProceedings of the 8th USENIX Conference on Operating Systems Design and Implementation(San Diego, California)(OSDI’08). USENIX Association, USA, 209–224

    2008

  16. [16]

    Păsăreanu, Koushik Sen, Nikolai Tillmann, and Willem Visser

    Cristian Cadar, Patrice Godefroid, Sarfraz Khurshid, Corina S. Păsăreanu, Koushik Sen, Nikolai Tillmann, and Willem Visser. 2011. Symbolic execution for software testing in practice: preliminary assessment. InProceedings of the 33rd International Conference on Software Engineering(Waikiki, Honolulu, HI, USA)(ICSE ’11). Association for Computing Machinery,...

    arXiv 2011

  17. [17]

    Cristian Cadar and Martin Nowack. 2021. KLEE symbolic execution engine in 2019.Int. J. Softw. Tools Technol. Transf. 23, 6 (Dec. 2021), 867–870. doi:10.1007/s10009-020-00570-3

    work page doi:10.1007/s10009-020-00570-3 2021

  18. [18]

    Cristian Cadar and Koushik Sen. 2013. Symbolic execution for software testing: three decades later.Commun. ACM56, 2 (Feb. 2013), 82–90. doi:10.1145/2408776.2408795

    arXiv 2013

  19. [19]

    Cristiano Calcagno and Dino Distefano. 2011. Infer: An Automatic Program Verifier for Memory Safety of C Programs. InNASA Formal Methods, Mihaela Bobaru, Klaus Havelund, Gerard J. Holzmann, and Rajeev Joshi (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 459–465

    2011

  20. [20]

    Sooyoung Cha, Seongjoon Hong, Junhee Lee, and Hakjoo Oh. 2018. Automatically generating search heuristics for concolic testing. InProceedings of the 40th International Conference on Software Engineering(Gothenburg, Sweden) (ICSE ’18). Association for Computing Machinery, New York, NY, USA, 1244–1254. doi:10.1145/3180155.3180166

    arXiv 2018

  21. [21]

    Jinbao Chen, Hongjing Xiang, Zuohong Zhao, Luhao Li, Yu Zhang, Boyao Ding, Qingwei Li, and Songyuan Xiong. 2025. Utilizing Precise and Complete Code Context to Guide LLM in Automatic False Positive Mitigation. arXiv:2411.03079 [cs.SE] https://arxiv.org/abs/2411.03079

    Pith/arXiv arXiv 2025

  22. [22]

    Directed Symbolic Execution for Vulnerability Discovery: An LLM-Guided Approach in KLEE

    Lingfeng Chen, Tao Xiao, Masanari Kondo, and Yasutaka Kamei. 2026. Replication package for "Directed Symbolic Execution for Vulnerability Discovery: An LLM-Guided Approach in KLEE". doi:10.5281/zenodo.21507662

    work page doi:10.5281/zenodo.21507662 2026

  23. [23]

    Vitaly Chipounov, Volodymyr Kuznetsov, and George Candea. 2011. S2E: a platform for in-vivo multi-path analysis of software systems. InProceedings of the Sixteenth International Conference on Architectural Support for Programming Languages and Operating Systems(Newport Beach, California, USA)(ASPLOS XVI). Association for Computing Machinery, New York, NY,...

    arXiv 2011

  24. [24]

    Yangruibo Ding, Yanjun Fu, Omniyyah Ibrahim, Chawin Sitawarin, Xinyun Chen, Basel Alomair, David Wagner, Baishakhi Ray, and Yizheng Chen. 2025. Vulnerability Detection with Code Language Models: How Far Are We?. In Proceedings of the IEEE/ACM 47th International Conference on Software Engineering(Ottawa, Ontario, Canada)(ICSE ’25). IEEE Press, 1729–1741. d...

    arXiv 2025

  25. [25]

    Xiaohu Du, Ming Wen, Jiahao Zhu, Zifan Xie, Bin Ji, Huijun Liu, Xuanhua Shi, and Hai Jin. 2024. Generalization- Enhanced Code Vulnerability Detection via Multi-Task Instruction Fine-Tuning. InFindings of the Association for Computational Linguistics: ACL 2024, Lun-Wei Ku, Andre Martins, and Vivek Srikumar (Eds.). Association for Compu- tational Linguistic...

    doi:10.18653/v1/2024.findings-acl.625 2024

  26. [26]

    Jianxiong Gao and Steven S. Lumetta. 2018. Loop path reduction by state pruning. InProceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering(Montpellier, France)(ASE ’18). Association for Computing Machinery, New York, NY, USA, 838–843. doi:10.1145/3238147.3240731

    arXiv 2018

  27. [27]

    A. Yu. Gerasimov. 2018. Directed Dynamic Symbolic Execution for Static Analysis Warnings Confirmation.Program- ming and Computer Software44, 5 (2018), 316–323. https://journals.rcsi.science/0361-7688/article/view/176654

    2018

  28. [28]

    GitHub. 2026. CodeQL Documentation. https://codeql.github.com/docs/. Accessed: 2026-06-25

    2026

  29. [29]

    google/sanitizers Wiki. 2019. AddressSanitizer. https://github.com/google/sanitizers/wiki/addresssanitizer. Accessed March 24, 2026

    2019

  30. [30]

    Daya Guo, Qihao Zhu, Dejian Yang, Zhenda Xie, Kai Dong, Wentao Zhang, Guanting Chen, Xiao Bi, Y. Wu, Y. K. Li, Fuli Luo, Yingfei Xiong, and Wenfeng Liang. 2024. DeepSeek-Coder: When the Large Language Model Meets Programming – The Rise of Code Intelligence. arXiv:2401.14196 [cs.SE] https://arxiv.org/abs/2401.14196

    Pith/arXiv arXiv 2024

  31. [31]

    Jingxuan He, Gishor Sivanrupan, Petar Tsankov, and Martin Vechev. 2021. Learning to Explore Paths for Symbolic Execution. InProceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security(Virtual Event, Republic of Korea)(CCS ’21). Association for Computing Machinery, New York, NY, USA, 2526–2540. doi:10. 1145/3460120.3484813

    arXiv 2021

  32. [32]

    Soneya Binta Hossain, Nan Jiang, Qiang Zhou, Xiaopeng Li, Wen-Hao Chiang, Yingjun Lyu, Hoan Nguyen, and Omer Tripp. 2024. A Deep Dive into Large Language Models for Automated Bug Localization and Repair.Proc. ACM Softw. Eng.1, FSE, Article 66 (July 2024), 23 pages. doi:10.1145/3660773

    doi:10.1145/3660773 2024

  33. [33]

    Brittany Johnson, Yoonki Song, Emerson Murphy-Hill, and Robert Bowdidge. 2013. Why don’t software developers use static analysis tools to find bugs? . In2013 35th International Conference on Software Engineering (ICSE). IEEE Computer Society, Los Alamitos, CA, USA, 672–681. doi:10.1109/ICSE.2013.6606613

    arXiv 2013

  34. [34]

    Timotej Kapus, Frank Busse, and Cristian Cadar. 2021. Pending constraints in symbolic execution for better exploration and seeding. InProceedings of the 35th IEEE/ACM International Conference on Automated Software Engineering(Virtual Event, Australia)(ASE ’20). Association for Computing Machinery, New York, NY, USA, 115–126. doi:10.1145/3324884. 3416589

    work page doi:10.1145/3324884 2021

  35. [35]

    Timotej Kapus, Oren Ish-Shalom, Shachar Itzhaky, Noam Rinetzky, and Cristian Cadar. 2019. Computing summaries of string loops in C for better testing and refactoring. InProceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation(Phoenix, AZ, USA)(PLDI 2019). Association for Computing Machinery, New York, NY, USA, 874–8...

    arXiv 2019

  36. [36]

    James C. King. 1976. Symbolic execution and program testing.Commun. ACM19, 7 (July 1976), 385–394. doi:10.1145/ 360248.360252

    arXiv 1976

  37. [37]

    KLEE. 2026. KLEE Documentation. https://klee-se.org/docs/. [Accessed 22-03-2026]

    2026

  38. [38]

    KLEE Project. 2017. KLEE issue 777. GitHub issue, https://github.com/klee/klee/issues/777

    2017

  39. [39]

    KLEE Project. 2018. KLEE issue 831. GitHub issue, https://github.com/klee/klee/issues/831

    2018

  40. [40]

    Rosmaël Zidane Lekeufack Foulefack and Alessandro Marchetto. 2026. Domain-aware Graph Neural Networks for Source Code Vulnerability Detection.Information and Software Technology195 (2026), 108104. doi:10.1016/j.infsof. 2026.108104

    arXiv 2026

  41. [41]

    Ahmed Lekssays, Hamza Mouhcine, Khang Tran, Ting Yu, and Issa Khalil. 2025. LLMxCPG: context-aware vulnerability detection through code property graph-guided large language models. InProceedings of the 34th USENIX Conference on Security Symposium(Seattle, WA, USA)(SEC ’25). USENIX Association, USA, Article 26, 19 pages

    2025

  42. [42]

    Matteo Leonelli, Addison Crump, Meng Wang, Florian Bauckholt, Keno Hassler, Ali Abbasi, and Thorsten Holz. 2025. TWINFUZZ: Differential Testing of Video Hardware Acceleration Stacks. InProceedings of the Network and Distributed System Security Symposium (NDSS 2025). Internet Society. doi:10.14722/ndss.2025.240526

    arXiv 2025

  43. [43]

    Yuwei Li, Shouling Ji, Yuan Chen, Sizhuang Liang, Wei-Han Lee, Yueyao Chen, Chenyang Lyu, Chunming Wu, Raheem Beyah, Peng Cheng, Kangjie Lu, and Ting Wang. 2021. UNIFUZZ: A Holistic and Pragmatic Metrics-Driven Platform for Evaluating Fuzzers. In30th USENIX Security Symposium (USENIX Security 21). USENIX Association, 2777–2794. https://www.usenix.org/conf...

    2021

  44. [44]

    You Li, Zhendong Su, Linzhang Wang, and Xuandong Li. 2013. Steering symbolic execution to less traveled paths. In Proceedings of the 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages ACM Trans. Softw. Eng. Methodol., Vol. 1, No. 1, Article . Publication date: July 2018. Directed Symbolic Execution for Vulnerability...

    arXiv 2013

  45. [45]

    Jie Lin and David Mohaisen. 2025. From Large to Mammoth: A Comparative Evaluation of Large Language Models in Vulnerability Detection. InProceedings of the Network and Distributed System Security Symposium (NDSS). Internet Society. doi:10.14722/ndss.2025.241491

    arXiv 2025

  46. [46]

    Pengfei Liu, Weizhe Yuan, Jinlan Fu, Zhengbao Jiang, Hiroaki Hayashi, and Graham Neubig. 2023. Pre-train, Prompt, and Predict: A Systematic Survey of Prompting Methods in Natural Language Processing.ACM Comput. Surv.55, 9, Article 195 (Jan. 2023), 35 pages. doi:10.1145/3560815

    doi:10.1145/3560815 2023

  47. [47]

    LLVM Project. 2025. AddressSanitizer. https://clang.llvm.org/docs/AddressSanitizer.html Accessed: 2026-03-25

    2025

  48. [48]

    LLVM Project. 2025. UndefinedBehaviorSanitizer. https://clang.llvm.org/docs/UndefinedBehaviorSanitizer.html Accessed: 2026-03-25

    2025

  49. [49]

    Foster, and Michael Hicks

    Kin-Keung Ma, Khoo Yit Phang, Jeffrey S. Foster, and Michael Hicks. 2011. Directed Symbolic Execution. InStatic Analysis, Eran Yahav (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 95–111

    2011

  50. [50]

    Jonathan Metzman, László Szekeres, Laurent Simon, Read Sprabery, and Abhishek Arya. 2021. FuzzBench: an open fuzzer benchmarking platform and service. InProceedings of the 29th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering(Athens, Greece)(ESEC/FSE 2021). Association for Computing Mac...

    arXiv 2021

  51. [51]

    MITRE. 2026. CWE-1399: CWE CATEGORY: Comprehensive Categorization: Memory Safety. https://cwe.mitre.org/ data/definitions/1399.html Accessed: 2026-03-25

    2026

  52. [52]

    MITRE. 2026. CWE-1406: CWE CATEGORY: Comprehensive Categorization: Improper Input Validation. https: //cwe.mitre.org/data/definitions/1406.html Accessed: 2026-03-25

    2026

  53. [53]

    MITRE. 2026. CWE-1417: CWE CATEGORY: Comprehensive Categorization: Sensitive Information Exposure. https: //cwe.mitre.org/data/definitions/1417.html Accessed: 2026-03-25

    2026

  54. [54]

    MITRE. 2026. CWE-362: Concurrent Execution using Shared Resource with Improper Synchronization (’Race Condi- tion’). https://cwe.mitre.org/data/definitions/362.html Accessed: 2026-03-25

    2026

  55. [55]

    MITRE. 2026. CWE-401: Missing Release of Memory after Effective Lifetime. https://cwe.mitre.org/data/definitions/ 401.html Accessed: 2026-03-25

    2026

  56. [56]

    MITRE. 2026. CWE-738: CWE CATEGORY: CERT C Secure Coding Standard (2008) Chapter 5 - Integers (INT). https://cwe.mitre.org/data/definitions/738.html Accessed: 2026-03-25

    2026

  57. [57]

    MITRE. 2026. CWE-742: CWE CATEGORY: CERT C Secure Coding Standard (2008) Chapter 9 - Memory Management (MEM). https://cwe.mitre.org/data/definitions/742.html Accessed: 2026-03-25

    2026

  58. [58]

    Chao Ni, Liyu Shen, Xiaohu Yang, Yan Zhu, and Shaohua Wang. 2024. MegaVul: A C/C++ Vulnerability Dataset with Comprehensive Code Representations. InProceedings of the 21st International Conference on Mining Software Repositories(Lisbon, Portugal)(MSR ’24). Association for Computing Machinery, New York, NY, USA, 738–742. doi:10.1145/3643991.3644886

    arXiv 2024

  59. [59]

    Chao Ni, Xin Yin, Xinrui Li, Xiaodan Xu, and Zhi Yu. 2026. Abundant Modalities Offer More Nutrients: Multi-Modal- Based Function-Level Vulnerability Detection.ACM Trans. Softw. Eng. Methodol.35, 2, Article 33 (Jan. 2026), 31 pages. doi:10.1145/3731557

    work page doi:10.1145/3731557 2026

  60. [60]

    Chao Ni, Xin Yin, Liyu Shen, and Shaohua Wang. 2025. Learning-based models for vulnerability detection: an extensive study.Empirical Softw. Engg.31, 1 (Nov. 2025), 35 pages. doi:10.1007/s10664-025-10734-x

    work page doi:10.1007/s10664-025-10734-x 2025

  61. [61]

    OpenAI. 2026. Prompt engineering. https://platform.openai.com/docs/guides/prompt-engineering. [Accessed 21-03-2026]

    2026

  62. [62]

    Xin Peng, Shangwen Wang, Yihao Qin, Bo Lin, Liqian Chen, and Xiaoguang Mao. 2024. Keep It Simple: Towards Accurate Vulnerability Detection for Large Code Graphs. arXiv:2412.10164 [cs.SE] https://arxiv.org/abs/2412.10164

    Pith/arXiv arXiv 2024

  63. [63]

    Wenting Qin, Lijie Suo, Liangchen Li, and Fan Yang. 2025. Advancing Software Vulnerability Detection with Reasoning LLMs: DeepSeek-R1’s Performance and Insights.Applied Sciences15, 12 (2025). doi:10.3390/app15126651

    work page doi:10.3390/app15126651 2025

  64. [64]

    Thomas Reps, Susan Horwitz, and Mooly Sagiv. 1995. Precise interprocedural dataflow analysis via graph reachability. InProceedings of the 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages(San Francisco, California, USA)(POPL ’95). Association for Computing Machinery, New York, NY, USA, 49–61. doi:10.1145/199448. 199462

    work page doi:10.1145/199448 1995

  65. [65]

    Caitlin Sadowski, Edward Aftandilian, Alex Eagle, Liam Miller-Cushon, and Ciera Jaspan. 2018. Lessons from building static analysis tools at Google.Commun. ACM61, 4 (March 2018), 58–66. doi:10.1145/3188720

    doi:10.1145/3188720 2018

  66. [66]

    Georgy Savidov and Andrey Fedotov. 2021. Casr-Cluster: Crash Clustering for Linux Applications. In2021 Ivannikov Ispras Open Conference (ISPRAS). 47–51. doi:10.1109/ISPRAS53967.2021.00012

    arXiv 2021

  67. [67]

    Semgrep. 2026. Semgrep Documentation. https://semgrep.dev/docs/. Accessed: 2026-06-25

    2026

  68. [68]

    Mohammed Latif Siddiq, Natalie Sekerak, Antonio Karam, Maria Leal, Arvin Islam-Gomes, and Joanna C. S. Santos

  69. [69]

    Yuqiang Sun, Daoyuan Wu, Yue Xue, Han Liu, Wei Ma, Lyuye Zhang, Yang Liu, and Yingjiu Li. 2025. LLM4Vuln: A Unified Evaluation Framework for Decoupling and Enhancing LLMs’ Vulnerability Reasoning. arXiv:2401.16185 [cs.CR] https://arxiv.org/abs/2401.16185

    Pith/arXiv arXiv 2025

  70. [70]

    Yue Sun, Guowei Yang, Shichao Lv, Zhi Li, and Limin Sun. 2024. Concrete Constraint Guided Symbolic Execution. InProceedings of the IEEE/ACM 46th International Conference on Software Engineering(Lisbon, Portugal)(ICSE ’24). Association for Computing Machinery, New York, NY, USA, Article 122, 12 pages. doi:10.1145/3597503.3639078

    arXiv 2024

  71. [71]

    Robert Tarjan. 1972. Depth-First Search and Linear Graph Algorithms.SIAM J. Comput.1, 2 (June 1972), 146–160. doi:10.1137/0201010

    doi:10.1137/0201010 1972

  72. [72]

    Wentong Tian, Yuanzhang Lin, Xiang Gao, and Hailong Sun. 2025. Enhanced Vulnerability Localization: Harmonizing Task-Specific Tuning and General LLM Prompting . In2025 IEEE International Conference on Software Maintenance and Evolution (ICSME). IEEE Computer Society, Los Alamitos, CA, USA, 110–122. doi:10.1109/ICSME64153.2025.00020

    arXiv 2025

  73. [73]

    David Trabish, Andrea Mattavelli, Noam Rinetzky, and Cristian Cadar. 2018. Chopped symbolic execution. InProceedings of the 40th International Conference on Software Engineering(Gothenburg, Sweden)(ICSE ’18). Association for Computing Machinery, New York, NY, USA, 350–360. doi:10.1145/3180155.3180251

    arXiv 2018

  74. [74]

    Haoxin Tu, Lingxiao Jiang, and Marcel Böhme. 2026. Vital: Vulnerability-Oriented Symbolic Execution via Type-Unsafe Pointer-Guided Monte Carlo Tree Search.ACM Trans. Softw. Eng. Methodol.(Jan. 2026). doi:10.1145/3786795 Just Accepted

    work page doi:10.1145/3786795 2026

  75. [75]

    Saad Ullah, Mingji Han, Saurabh Pujar, Hammond Pearce, Ayse Coskun, and Gianluca Stringhini. 2024. LLMs Cannot Reliably Identify and Reason About Security Vulnerabilities (Yet?): A Comprehensive Evaluation, Framework, and Benchmarks . In2024 IEEE Symposium on Security and Privacy (SP). IEEE Computer Society, Los Alamitos, CA, USA, 862–880. doi:10.1109/SP5...

    arXiv 2024

  76. [76]

    Jiayi Wang, Ping Yu, Yi Qin, Yanyan Jiang, Yuan Yao, and Xiaoxing Ma. 2025. NexuSym: Marrying symbolic path finders with large language models.Automated Software Engg.32, 2 (June 2025), 29 pages. doi:10.1007/s10515-025-00529-1

    work page doi:10.1007/s10515-025-00529-1 2025

  77. [77]

    Xuezhi Wang, Jason Wei, Dale Schuurmans, Quoc Le, Ed Chi, Sharan Narang, Aakanksha Chowdhery, and Denny Zhou. 2023. Self-Consistency Improves Chain of Thought Reasoning in Language Models. InThe Eleventh International Conference on Learning Representations. https://openreview.net/forum?id=1PL1NIMMrw

    2023

  78. [78]

    Chi, Quoc V

    Jason Wei, Xuezhi Wang, Dale Schuurmans, Maarten Bosma, Brian Ichter, Fei Xia, Ed H. Chi, Quoc V. Le, and Denny Zhou. 2022. Chain-of-thought prompting elicits reasoning in large language models. InProceedings of the 36th International Conference on Neural Information Processing Systems(New Orleans, LA, USA)(NIPS ’22). Curran Associates Inc., Red Hook, NY,...

    2022

  79. [79]

    Qiushi Wu, Aditya Pakki, Navid Emamdoost, Stephen McCamant, and Kangjie Lu. 2021. Understanding and Detecting Disordered Error Handling with Precise Function Pairing. In30th USENIX Security Symposium (USENIX Security 21). USENIX Association, 2041–2058

    2021

  80. [80]

    Wei-Cheng Wu, Stefan Nagy, and Christophe Hauser. 2025. WildSync: Automated Fuzzing Harness Synthesis via Wild API Usage Recovery.Proc. ACM Softw. Eng.2, ISSTA, Article ISSTA043 (June 2025), 22 pages. doi:10.1145/3728918

    work page doi:10.1145/3728918 2025

Showing first 80 references.