Pith. sign in

REVIEW 4 major objections 34 references

Reasoning LLMs with consistency checks and reasoning evaluation can adjudicate static-analysis alerts at high recall and high specificity on three benchmark suites.

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 · grok-4.5

2026-07-14 01:17 UTC pith:3RTJ7EIQ

load-bearing objection Careful empirical SE paper with a real tool and honest memorization analysis; FormAI labels are partly LLM-influenced but the circularity is overstated relative to the rest of the evidence. the 4 major comments →

arxiv 2607.09979 v1 pith:3RTJ7EIQ submitted 2026-07-10 cs.SE

Using LLMs to Adjudicate Static-Analysis Alerts with Error Reduction Techniques

William Klieber , David Svoboda , Lori Flynn , Ruben Martins This is my paper
classification cs.SE
keywords static analysisalert adjudicationlarge language modelsfalse-positive reductionconsistency checkLLM reasoning evaluationsecurity weaknessesdynamic trigger test
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.

Static analyzers find security weaknesses before code ships, but they flood teams with more alerts than humans can review, and many of those alerts are false. This paper asks whether modern reasoning large language models can take over much of that adjudication work—labeling each alert as a real bug, a dependent symptom, a false alarm, or uncertain—and still keep almost every real bug while discarding most false alarms. The authors build an open pipeline, LASAA, that feeds the model the alert and the surrounding function, lets the model request missing definitions, and returns a verdict plus written reasoning. To cut model mistakes they add a consistency check over multiple independent runs and an optional second step in which the model re-reads its own discordant replies and picks a better-supported answer. On Juliet, FormAI, and SV-COMP, mid-tier reasoning models with these mitigations reach at least 98 percent recall and at least 94.8 percent specificity on every suite. Because Juliet appears memorized, they rest generalization claims mainly on FormAI, scored against their own unpublished manual labels; a separate dynamic-trigger test that synthesizes a driver to fire the flaw never produced a valid trigger for a false alarm, so a valid trigger is strong independent evidence of a real bug.

Core claim

When mid-tier reasoning LLMs adjudicate static-analysis alerts and their answers are filtered by a multi-run consistency check—and, on the hardest suite, by an additional self-evaluation of competing reasoning—they keep at least 98 percent of real bugs for human attention and correctly dismiss at least 94.8 percent of false alarms on Juliet, FormAI, and SV-COMP, turning a large unreviewed alert backlog into a much smaller, higher-confidence set.

What carries the argument

LASAA’s two-stage mistake mitigation: a consistency check that requires a high fraction of independent trials to agree before accepting a verdict (otherwise returning “uncertain”), optionally preceded by LLM reasoning evaluation, which re-prompts the model on its own discordant replies and asks it to weigh the reasoning rather than simply majority-vote.

Load-bearing premise

That high accuracy on small samples drawn from synthetic, LLM-generated, and hand-crafted suites—scored partly against unpublished manual labels and without alerts from real static analyzers—predicts how the same pipeline will behave on large production codebases.

What would settle it

Run the same pipeline, with the same models and thresholds, on a large corpus of alerts produced by widely used static analyzers on real open-source or industrial C/C++ codebases whose true/false labels have been independently audited; if recall or specificity falls substantially below the reported floors, the operational claim fails.

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

If this is right

  • Analysts can discard only alerts the pipeline confidently labels false and focus limited review time on true, dependent, and uncertain cases.
  • Dependent labels point developers at the single upstream line that needs fixing instead of every downstream symptom.
  • A valid dynamic trigger can be used to prioritize confirmed true positives at the front of the repair queue.
  • Open-weight mid-tier reasoning models become practical local adjudicators when code cannot leave the premises.
  • Consistency-check thresholds and trial counts give operators an explicit knob trading missed flaws against review burden and token cost.

Where Pith is reading between the lines

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

  • If the same mitigation pattern works for other high-volume triage tasks (linter noise, dependency-vulnerability alerts, CI flaky-test reports), a reusable “reason-then-reconcile” pattern could become standard for LLM safety filters.
  • The gap between high benchmark specificity and the still-modest fraction of true positives that produce a valid trigger suggests that execution-based confirmation and static adjudication will remain complementary rather than interchangeable.
  • Because LRE sometimes hurts when the original prompt is ambiguous, prompt-clarity work may be as important as model scale for operational deployment.
  • Adaptive early-stopping of trials once a clear majority appears would cut token cost without changing the decision rule.

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 / 0 minor

Summary. The paper introduces LASAA, an analyzer-agnostic pipeline that uses LLMs to adjudicate static-analysis alerts as true, false, dependent, or uncertain, and studies two mistake-mitigation methods: a multi-trial consistency check (CC) and an LLM reasoning evaluation (LRE) step that re-weighs discordant trial reasoning. On Juliet, FormAI, and SV-COMP, mid-tier reasoning models (o4-mini, gpt-oss-120b, gpt-oss-20b) with mitigation reach at least 98% recall and at least 94.8% specificity (CC alone on Juliet/SV-COMP; LRE+CC on FormAI). The authors probe Juliet memorization via filename reconstruction and a flipped-verdict experiment, base generalization primarily on FormAI scored against their own manual labels, release the tool, and add a validity-checked dynamic trigger test as independent evidence of true positives.

Significance. If the reported rates transfer beyond the evaluated suites, the work would matter for high-assurance triage: most real flaws would be retained for human attention while most false alarms could be filtered, reducing unreviewed residual risk. Strengths that should be credited include the open LASAA artifact, class-conditional recall/specificity (rather than prevalence-dependent precision alone), majority-vote baselines, Clopper–Pearson intervals, an explicit memorization probe (Table 6), the flipped-verdict experiment, and a trigger test whose validity check rejected every driver aimed at a false alarm. LRE is a clear, well-motivated variant of self-consistency/USC that can prefer a better-reasoned minority. The main significance is therefore empirical and engineering: a careful measurement of modern reasoning LLMs on alert adjudication, with usable mitigation knobs and released code.

major comments (4)
  1. Abstract and §6.3–6.4 rest generalization primarily on FormAI, but §6.2 and Table 5 show that seven FormAI manual labels were revised after reviewing LLM justifications or trigger outcomes. Because the same model family under evaluation helped reshape the answer key, the headline ≥98% recall / ≥94.8% specificity rates on FormAI are not fully independent of the adjudicator. For a load-bearing generalization claim, the paper should either (a) freeze and release a pre-LLM label set and report both pre- and post-revision scores, or (b) obtain independent re-adjudication by humans who never see LLM output, and treat LLM-influenced flips as a sensitivity analysis rather than the primary key.
  2. §9 and §6.1 state that none of the three evaluations used alerts produced by a real static analyzer: Juliet and SV-COMP ask whether a CWE/property occurs anywhere in the case, and FormAI uses ESBMC-style categories/messages that differ from typical SA output. The central operational claim is about adjudicating static-analysis alerts. Without at least one experiment on SARIF/CodeQL/Clang/etc. alerts from non-benchmark code, the suite-level rates cannot support that claim as stated. This is fixable in scope by adding a modest real-analyzer study or by substantially narrowing the abstract/conclusion claims to “benchmark alert-like tasks.”
  3. §6.1 and §9: FormAI specificity is estimated on only 27 actually-false alerts (76 total after filtering), and Juliet/SV-COMP samples are 100/101 cases. The paper’s own pooled intervals and limitations text already show that whole-suite extrapolation is weak. The abstract’s “on every suite” phrasing still reads as a strong suite-level guarantee. Either enlarge the actually-false FormAI sample (and report per-CWE/category breakdowns more prominently, cf. Table 9) or rephrase the headline claim to the sampled subsets with explicit uncertainty, so the central quantitative claim matches the statistical support.
  4. §6.3 Table 6 shows high residual case identity after sanitization (o4-mini exact functional variant 68%; ≥2 on 91%), while the flipped-verdict experiment covers only 20 cases and still leaves templates recognizable. The paper correctly de-emphasizes Juliet, but Tables 3–4 and the abstract still present Juliet rates alongside FormAI/SV-COMP as part of the “every suite” claim. Juliet results should be clearly labeled as contaminated/upper-bound evidence in the abstract and result summary, not as co-equal support for generalization.

Circularity Check

1 steps flagged

Empirical classification rates against mostly external or independently revised labels; only mild evaluation contamination from a handful of FormAI label flips influenced by the models under test.

specific steps
  1. other [§6.2 Ground truth and its difficulty; Table 5; Abstract (FormAI scoring claim)]
    "Even careful manual adjudications were not final. Modern LLMs are now good enough that, when an LLM disagrees with a manual adjudication, it is sometimes the manual adjudication that is wrong: the LLM’s written justification (and for true positives, the dynamic trigger test of Sec. 5) repeatedly revealed genuine mistakes in our own adjudications and convinced us to revise them. Table 5 lists the FormAI alerts whose manual adjudication we changed after reviewing LLM output or trigger results. ... we base our generalization claims primarily on FormAI, scored against our own unpublished manual ad"

    Seven FormAI ground-truth labels (out of 76) were flipped after inspecting outputs of the same LLM family later scored on those labels. This makes a minority of the FormAI evaluation key partially dependent on the adjudicator under test, so the reported FormAI rates are not fully independent measurements. It is evaluation contamination rather than a derivation that equals its inputs by construction; the bulk of labels and the other two suites remain external.

full rationale

This is an empirical measurement paper, not a first-principles derivation. The central claims are class-conditional rates (recall, specificity) of LLM adjudicators on three suites, obtained by running the models and scoring against answer keys. Juliet and SV-COMP keys are external (with one documented Juliet CWE relabel). FormAI uses the authors' unpublished three-way manual labels; seven of 76 were revised after LLM justifications or trigger tests (Table 5, §6.2), which introduces mild contamination because the same model family helped shape a minority of the scoring key. That is a validity/threat-to-independence issue the paper itself surfaces, not a reduction of a claimed prediction to its inputs by construction, a fitted parameter renamed as prediction, a load-bearing self-citation uniqueness theorem, or an ansatz smuggled via citation. No equations equate a derived quantity to a fitted input; no uniqueness is imported from the authors' prior work to force the result; related-work citations are ordinary. The headline rates therefore remain empirical measurements, not tautologies. Score 2 reflects the documented FormAI label influence without elevating it to central circularity.

Axiom & Free-Parameter Ledger

3 free parameters · 5 axioms · 2 invented entities

This is an empirical systems paper. Load-bearing premises are experimental design choices and ground-truth conventions rather than physical axioms. Free parameters are the CC thresholds, trial counts, and sampling settings chosen by the authors. Domain assumptions include treating uncertain/dependent as positive for recall/specificity and the FormAI manual labels as truth. No new physical entities are postulated.

free parameters (3)
  • CC threshold (default 80%, also 70%/90% in places)
    Chosen by hand (initially per-LLM to keep wrong answers <5%, later uniform 80% before revised runs). Directly controls the recall/specificity/uncertain tradeoff that the headline numbers depend on.
  • Number of trials N1/N2 (typically 10; 5 for some frontier models)
    Author-chosen sample size for consistency and LRE; affects both cost and whether the consistency check can fire.
  • FormAI sample and manual adjudication labels (76 alerts after filtering)
    Unpublished human labels, revised after LLM/trigger feedback, form the primary generalization ground truth; not a fitted continuous parameter but a free labeling choice the central FormAI claim rests on.
axioms (5)
  • domain assumption Adjudication is scored as a binary classifier with positive class = real flaw present; dependent and uncertain count as positive for recall/specificity.
    Stated in §2 and Metrics §6; defines the headline rates and treats uncertain as weak positive because false negatives are costlier.
  • domain assumption Authors’ unpublished manual FormAI adjudications (after revisions in Table 5) are the correct ground truth for generalization claims.
    §6.2 and abstract: FormAI’s ESBMC key is rejected; claims rest on these labels.
  • domain assumption Sanitized Juliet still allows fair measurement of reasoning when combined with flipped-verdict checks, but memorization risk is high enough that FormAI should carry generalization.
    §6.3 memorization probe and flipped-verdict experiment; authors themselves demote Juliet for generalization.
  • domain assumption A trigger driver that fires at the flagged line and passes the LLM validity check is strong evidence of a true positive; absence of a trigger is not exoneration.
    §5 and §6.7; validity check rejected all false-positive drivers in their sample.
  • ad hoc to paper Default provider sampling settings and (for some models) high reasoning effort are acceptable evaluation conditions.
    §6: temperature not set; o4-mini left at default reasoning effort by accident.
invented entities (2)
  • LASAA pipeline (CC + optional LRE adjudication loop) independent evidence
    purpose: Operational system that turns SA alerts into LLM verdicts with justifications and optional dynamic triggers.
    Software artifact, not a scientific entity; independent evidence is the public GitHub release and reported benchmark tables.
  • LLM Reasoning Evaluation (LRE) step independent evidence
    purpose: Second-phase prompt that reconciles discordant multi-run adjudications by weighing reasoning rather than majority vote.
    Methodological construct closely related to USC/LLM-as-judge; evidence is FormAI gains vs CC-only and the car-wash toy experiment.

pith-pipeline@v1.1.0-grok45 · 35655 in / 3686 out tokens · 32789 ms · 2026-07-14T01:17:32.437355+00:00 · methodology

0 comments
read the original abstract

Static analysis is widely used for finding security weaknesses in source code before deployment, but it often produces far more alerts than analysts can review. We study how well large language models (LLMs) can adjudicate (classify as a real bug or a false alarm) static-analysis alerts. We use two mistake-mitigation methods: (1) a consistency check (CC) that runs the LLM multiple times and checks that the verdicts are consistent with each other, and (2) an LLM reasoning evaluation (LRE) step that runs the LLM multiple times and then asks the LLM to choose a verdict after evaluating the reasoning provided by each run. We evaluated several LLMs on three test suites: Juliet, FormAI, and SV-COMP. Across all three suites, the mid-tier reasoning LLMs that we tested (o4-mini, gpt-oss-120b, gpt-oss-20b) reach high recall (percent of real bugs that the tool correctly flags as needing repair / manual attention) and specificity (percent of actually false alerts that the tool correctly dismisses as false alarms). With mistake mitigation, they reach at least 98% recall and at least 94.8% specificity on every suite (with CC alone on Juliet and SV-COMP, and with LRE+CC on FormAI). We probe Juliet memorization and show that o4-mini can often reconstruct sanitized test cases' original identities, so we base our generalization claims primarily on FormAI, scored against our own unpublished manual adjudications. We also report results of using the LLM to synthesize a program that dynamically triggers the flaw as independent evidence; a validity check rejected every trigger driver aimed at a false alarm, so a valid trigger proved to be strong evidence of a real flaw.

Figures

Figures reproduced from arXiv: 2607.09979 by David Svoboda, Lori Flynn, Ruben Martins, William Klieber.

Figure 1
Figure 1. Figure 1: LASAA pipeline Run trial 1 Test case Run trial 2 Run trial N … Reply 1 Reply 2 … Reply N Consistency Check Final Answer [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Consistency check. “// Line N” annotations appended, and (C) instruc￾tions on what to do. The LLM is instructed to ask for definitions of macros and structs that it needs. If the LLM makes such a re￾quest, LASAA locates the definition of the macro/struct (using ctags1 ) and re-runs the prompt with the defini￾tion appended. (This functionality was not exercised by the benchmarks in the Evaluation section, b… view at source ↗
Figure 3
Figure 3. Figure 3: Combining LLM reasoning evaluation with consistency check Repl. 1 2 3 4 5 6 7 8 9 10 TOTAL Orig 5/10 2/10 1/10 1/10 1/10 2/10 3/10 1/10 0/10 3/10 19/100 LRE 10/10 10/10 10/10 10/10 10/10 10/10 10/10 9/10 — 10/10 89/90 [PITH_FULL_IMAGE:figures/full_fig_p004_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Pseudocode for CC and LRE, where N1 and N2 are the number of times to run the orig query and the LRE query, respectively; see Sec. 3.3.4 for details. The function ask_LLM(query, N) sends query to the LLM N times and returns the N replies from the LLM. agreed on “walk” as the verdict, so LRE was skipped for that replication. In the other 9 replications, we ran LRE 10 times. The results for each replication … view at source ↗
Figure 5
Figure 5. Figure 5: Code excerpt from FormAI alert 068671 signed-integer bit-width, there is only one case where division overflows: dividing the most nega￾tive representable value by −1.) 3. Clarified that undefined behavior in the definition of a value should be flagged at the definition rather than at a later use, and that tenuously related un￾defined behavior (UB) should be ignored. 4. Clarified how to treat a signed-inte… 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

34 extracted references · 1 canonical work pages

  1. [1]

    Assisting static analysis with large language models: A ChatGPT experiment

    Haonan Li, Yu Hao, Yizhuo Zhai, and Zhiyun Qian. Assisting static analysis with large language models: A ChatGPT experiment. InProc. ACM Joint European Software Engineering Conf. and Symp. on the Foun- dations of Software Engineering (ESEC/FSE), 2023. doi:10.1145/3611643.3613078

    doi:10.1145/3611643.3613078 2023

  2. [2]

    Automatically inspecting thousands of static bug warnings with large language model: How far are we?ACM Trans

    Cheng Wen, Yuandao Cai, Bin Zhang, Jie Su, Zhiwu Xu, Dugang Liu, Shengchao Qin, Zhong Ming, and Cong Tian. Automatically inspecting thousands of static bug warnings with large language model: How far are we?ACM Trans. on Knowledge Discovery from Data (TKDD), 2024.doi:10.1145/3653718

    doi:10.1145/3653718 2024

  3. [3]

    Reducing false positives in static bug detection with LLMs: An empirical study in indus- try, 2026

    Xueying Du et al. Reducing false positives in static bug detection with LLMs: An empirical study in indus- try, 2026. URL:https://arxiv.org/abs/2601.18844, arXiv:2601.18844

    arXiv 2026

  4. [4]

    Common weakness enumeration (CWE)

    MITRE. Common weakness enumeration (CWE). https://cwe.mitre.org/, 2024

    2024

  5. [5]

    Static analysis alert audits: Lexicon & rules

    David Svoboda, Lori Flynn, and Will Snavely. Static analysis alert audits: Lexicon & rules. In2016 IEEE Cybersecurity Development (SecDev), pages 37–44. IEEE, 2016.https://www.sei.cmu.edu/documents/ 1476/2016_021_001_484193.pdf

    2016

  6. [6]

    Twitter, Feb 9, 2026.https://x.com/ WishinElarion/status/2020766452782157950

    @WishinElarion. Twitter, Feb 9, 2026.https://x.com/ WishinElarion/status/2020766452782157950

    arXiv 2026

  7. [7]

    Twitter, Feb 10, 2026.https://x

    @Shitty_Future. Twitter, Feb 10, 2026.https://x. com/Shitty_Future/status/2021327892148269295

    arXiv 2026

  8. [8]

    car-wash-evals

    Ryan Allen. car-wash-evals. GitHub repository, 2026. https://github.com/ryan-allen/car-wash-evals

    2026

  9. [9]

    Univer- sal self-consistency for large language model genera- tion, 2023

    Xinyun Chen, Renat Aksitov, Uri Alon, Jie Ren, Ke- fan Xiao, Pengcheng Yin, Sushant Prakash, Charles Sutton, Xuezhi Wang, and Denny Zhou. Univer- sal self-consistency for large language model genera- tion, 2023. URL:https://arxiv.org/abs/2311.17311, arXiv:2311.17311

    Pith/arXiv arXiv 2023

  10. [10]

    Auditing multi-agent LLM reasoning trees outperforms majority vote and LLM-as-judge, 2026

    Wei Yang, Shixuan Li, Heng Ping, Peiyu Zhang, Paul Bogdan, and Jesse Thomason. Auditing multi-agent LLM reasoning trees outperforms majority vote and LLM-as-judge, 2026. URL:https://arxiv.org/abs/ 2602.09341,arXiv:2602.09341

    arXiv 2026

  11. [11]

    Xing, Hao Zhang, Joseph E

    Lianmin Zheng, Wei-Lin Chiang, Ying Sheng, Siyuan Zhuang, Zhanghao Wu, Yonghao Zhuang, Zi Lin, Zhuo- han Li, Dacheng Li, Eric P. Xing, Hao Zhang, Joseph E. Gonzalez, and Ion Stoica. Judging LLM-as-a-Judge with MT-Bench and Chatbot Arena. InNeurIPS Datasets and Benchmarks Track, 2023. URL:https: //arxiv.org/abs/2306.05685,arXiv:2306.05685

    Pith/arXiv arXiv 2023

  12. [12]

    A survey on LLM-as-a-Judge,

    Jiawei Gu et al. A survey on LLM-as-a-Judge,

  13. [13]

    URL:https://arxiv.org/abs/2411.15594, arXiv:2411.15594

    Pith/arXiv arXiv

  14. [14]

    Self-consistencyimproveschainofthought reasoning in language models, 2022

    Xuezhi Wang, Jason Wei, Dale Schuurmans, Quoc Le, Ed Chi, Sharan Narang, Aakanksha Chowdhery, and DennyZhou. Self-consistencyimproveschainofthought reasoning in language models, 2022. URL:https:// arxiv.org/abs/2203.11171,arXiv:2203.11171

    Pith/arXiv arXiv 2022

  15. [15]

    Bowman, and Shi Feng

    Arjun Panickssery, Samuel R. Bowman, and Shi Feng. LLM evaluators recognize and favor their own genera- tions. InAdvances in Neural Information Processing Systems 37 (NeurIPS 2024), 2024. URL:https:// arxiv.org/abs/2404.13076,arXiv:2404.13076,doi: 10.52202/079017-2197

    Pith/arXiv arXiv doi:10.52202/079017-2197 2024

  16. [16]

    AddressSanitizer and UndefinedBehav- iorSanitizer.https://clang.llvm.org/docs/, 2024

    LLVM Project. AddressSanitizer and UndefinedBehav- iorSanitizer.https://clang.llvm.org/docs/, 2024

    2024

  17. [17]

    Juliet C/C++ test suite, software assurance reference dataset (SARD).https://samate.nist.gov/SARD/, 2017

    National Institute of Standards and Technology. Juliet C/C++ test suite, software assurance reference dataset (SARD).https://samate.nist.gov/SARD/, 2017. 21[Distribution Statement A] Approved for public release and unlimited distribution

    2017

  18. [18]

    Cordeiro, and Vasileios Mavroeidis

    Norbert Tihanyi, Tamas Bisztray, Ridhi Jain, Mo- hamed Amine Ferrag, Lucas C. Cordeiro, and Vasileios Mavroeidis. TheFormAIdataset: GenerativeAIinsoft- ware security through the lens of formal verification. In Proc. 19th Int. Conf. on Predictive Models and Data Analytics in Software Engineering (PROMISE), 2023. doi:10.1145/3617555.3617874

    doi:10.1145/3617555.3617874 2023

  19. [19]

    Cordeiro

    Norbert Tihanyi, Tamas Bisztray, Mohamed Amine Ferrag, Ridhi Jain, and Lucas C. Cordeiro. How se- cure is AI-generated code: a large-scale comparison of large language models.Empirical Software Engineering, 30(47), 2025.doi:10.1007/s10664-024-10590-1

    doi:10.1007/s10664-024-10590-1 2025

  20. [20]

    SMT-based bounded model checking for embed- ded ANSI-C software.IEEE Transactions on Software Engineering, 38(4):957–974, 2012.doi:10.1109/TSE

    Lucas Cordeiro, Bernd Fischer, and João Marques- Silva. SMT-based bounded model checking for embed- ded ANSI-C software.IEEE Transactions on Software Engineering, 38(4):957–974, 2012.doi:10.1109/TSE. 2011.59

    doi:10.1109/tse 2012

  21. [21]

    Mikhail Y. R. Gadelha, Felipe R. Monteiro, Jeremy Morse, Lucas C. Cordeiro, Bernd Fischer, and Denis A. Nicole. ESBMC 5.0: An industrial-strength C model checker. InProc. 33rd ACM/IEEE Int. Conf. on Au- tomated Software Engineering (ASE), pages 888–891, 2018.doi:10.1145/3238147.3240481

    doi:10.1145/3238147.3240481 2018

  22. [22]

    ESBMC v7.4: Harnessing the power of intervals: (competition contribution)

    Rafael Sá Menezes, Mohannad Aldughaim, Bruno Farias, Xianzhiyu Li, Edoardo Manino, Fedor Shmarov, Kunjian Song, Franz Brauße, Mikhail R Gadelha, Nor- bert Tihanyi, et al. ESBMC v7.4: Harnessing the power of intervals: (competition contribution). InIn- ternational Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 376–38...

    2024

  23. [23]

    State of the art in software verification and witness validation: SV-COMP 2024

    Dirk Beyer. State of the art in software verification and witness validation: SV-COMP 2024. InTools and Al- gorithms for the Construction and Analysis of Systems (TACAS), 2024.doi:10.1007/978-3-031-57256-2_15

    work page doi:10.1007/978-3-031-57256-2_15 2024

  24. [24]

    The security risk of lacking compiler protec- tion in WebAssembly

    Quentin Stiévenart, Coen De Roover, and Mohammad Ghafari. The security risk of lacking compiler protec- tion in WebAssembly. In2021 IEEE 21st International Conference on Software Quality, Reliability and Secu- rity (QRS), pages 132–139. IEEE, 2021

    2021

  25. [25]

    The hitchhiker’s guide to program analysis: A jour- ney with large language models, 2023

    Haonan Li, Yu Hao, Yizhuo Zhai, and Zhiyun Qian. The hitchhiker’s guide to program analysis: A jour- ney with large language models, 2023. URL:https: //arxiv.org/abs/2308.00245,arXiv:2308.00245

    Pith/arXiv arXiv 2023

  26. [26]

    En- hancing static analysis for practical bug detection: An LLM-integrated approach.Proc

    Haonan Li, Yu Hao, Yizhuo Zhai, and Zhiyun Qian. En- hancing static analysis for practical bug detection: An LLM-integrated approach.Proc. ACM Program. Lang. (OOPSLA), 2024.doi:10.1145/3649828

    doi:10.1145/3649828 2024

  27. [27]

    The hitchhiker’s guide to program analysis, part II: Deep thoughts by LLMs, 2025

    Haonan Li, Hang Zhang, Kexin Pei, and Zhiyun Qian. The hitchhiker’s guide to program analysis, part II: Deep thoughts by LLMs, 2025. URL:https://arxiv. org/abs/2504.11711,arXiv:2504.11711

    Pith/arXiv arXiv 2025

  28. [28]

    ZeroFalse: Improving preci- sion in static analysis with LLMs, 2025

    Mohsen Iranmanesh et al. ZeroFalse: Improving preci- sion in static analysis with LLMs, 2025. URL:https: //arxiv.org/abs/2510.02534,arXiv:2510.02534

    arXiv 2025

  29. [29]

    Towards effective comple- mentary security analysis using large language mod- els, 2025

    Jonas Wagner et al. Towards effective comple- mentary security analysis using large language mod- els, 2025. URL:https://arxiv.org/abs/2506.16899, arXiv:2506.16899

    Pith/arXiv arXiv 2025

  30. [30]

    Minimizing false positives in static bug detection via LLM-enhanced path feasibility analy- sis, 2025

    Xueying Du et al. Minimizing false positives in static bug detection via LLM-enhanced path feasibility analy- sis, 2025. URL:https://arxiv.org/abs/2506.10322, arXiv:2506.10322

    Pith/arXiv arXiv 2025

  31. [31]

    Utilizing precise and complete code contexttoguideLLMinautomaticfalsepositivemitiga- tion, 2024

    Jinbao Chen et al. Utilizing precise and complete code contexttoguideLLMinautomaticfalsepositivemitiga- tion, 2024. URL:https://arxiv.org/abs/2411.03079, arXiv:2411.03079

    Pith/arXiv arXiv 2024

  32. [32]

    IRIS: LLM- assistedstaticanalysisfordetectingsecurityvulnerabili- ties, 2024

    Ziyang Li, Saikat Dutta, and Mayur Naik. IRIS: LLM- assistedstaticanalysisfordetectingsecurityvulnerabili- ties, 2024. URL:https://arxiv.org/abs/2405.17238, arXiv:2405.17238

    Pith/arXiv arXiv 2024

  33. [33]

    Code- CureAgent: Automatic classification and repair of static analysis warnings, 2025

    Pascal Joos, Islem Bouzenia, and Michael Pradel. Code- CureAgent: Automatic classification and repair of static analysis warnings, 2025. URL:https://arxiv. org/abs/2509.11787,arXiv:2509.11787

    Pith/arXiv arXiv 2025

  34. [34]

    Lemur: Integratinglargelanguagemodelsinautomated program verification, 2023

    Haoze Wu, Clark Barrett, and Nina Narodytska. Lemur: Integratinglargelanguagemodelsinautomated program verification, 2023. URL:https://arxiv.org/ abs/2310.04870,arXiv:2310.04870. 22[Distribution Statement A] Approved for public release and unlimited distribution

    Pith/arXiv arXiv 2023