Pith. sign in

REVIEW 2 major objections 2 minor 51 references

An LLM extracts per-function dataflow facts that Datalog composes and SMT filters to rediscover CVEs and synthesize crashes without building the code.

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.3

2026-06-28 18:36 UTC pith:EWSHURLY

load-bearing objection NeuroLog reports concrete ASan-confirmed bugs from curl and libarchive via an LLM-Datalog-SMT no-build pipeline, but provides no quantitative check on LLM fact accuracy. the 2 major comments →

arxiv 2606.00669 v1 pith:EWSHURLY submitted 2026-05-30 cs.CR

NeuroLog: Reasoning You Can Audit -- Neuro-Symbolic Vulnerability Discovery via LLM Facts, Datalog, and SMT

Sanjay Rawat This is my paper
classification cs.CR
keywords vulnerability discoveryneuro-symbolic analysisLLM fact extractionDatalog compositionSMT filteringcrash synthesisbuild-free analysisC/C++ security
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.

The paper presents NeuroLog as a build-free pipeline that lets an LLM pull typed dataflow facts from individual C/C++ functions one at a time. A Souffle Datalog mesh then links those facts into cross-function findings, Z3 SMT removes infeasible ones while producing SAT models, and a second LLM turns the models into Python programs that generate candidate inputs tested under AddressSanitizer. Runtime range invariants from a few corpus seeds are folded in to tighten the constraints at low cost. This layered approach matters because pure static tools demand compilable builds while standalone LLMs lose track of dataflow and invent details. The method rediscovers eight CVE-class issues including the CVSS-9.8 CVE-2023-38545 and reports five memory-safety bugs in libarchive HEAD, several of which received upstream fixes.

Core claim

NeuroLog assigns an LLM the task of extracting typed dataflow facts one function at a time from source code, uses a Datalog rule mesh to compose those facts into cross-function findings, applies Z3 to filter infeasible ones and emit SAT models, incorporates runtime invariants from seeds, and has a second LLM synthesize crashing inputs from the models. This end-to-end process rediscovers eight CVE-class issues including CVE-2023-38545 and surfaces five memory-safety bugs in libarchive HEAD, with several fixes merged upstream.

What carries the argument

The LLM-derived fact base composed by Souffle Datalog rules and refined by Z3 SMT solvers, with SAT models serving as direct input to LLM-based crash synthesis.

Load-bearing premise

The LLM extracts accurate typed dataflow facts one function at a time that are complete enough for the Datalog rules to compose into correct cross-function findings without missing or inventing critical details.

What would settle it

A case in which the LLM misses or invents a dataflow fact for a known vulnerability, causing the Datalog rules and SMT pass to produce either a false negative or an invalid finding that survives filtering.

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

If this is right

  • Static findings become concrete crashing inputs after a small number of LLM iterations that emit Python programs, as shown with a 102-byte stb_vorbis crash.
  • A handful of runtime seeds can eliminate a measurable fraction of the feasible set, such as 13.2 percent for the FFmpeg demuxer.
  • The pipeline operates on real libraries including curl 8.3.0 and libarchive HEAD without requiring any build step.
  • Extraction cost stays low, around 37 seconds and $0.005 on stb, while still surfacing actionable memory-safety issues that reach upstream acknowledgment in hours.

Where Pith is reading between the lines

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

  • If fact extraction scales reliably to larger modules, the method could open static analysis to projects that resist standard builds.
  • SAT models produced as artifacts could supply high-quality seeds to fuzzers instead of relying solely on mutation.
  • Adding more classes of runtime evidence beyond range invariants might further reduce the SMT search space on complex codebases.

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

2 major / 2 minor

Summary. The paper presents NeuroLog, a build-free neuro-symbolic pipeline for C/C++ vulnerability discovery. An LLM extracts typed dataflow facts one function at a time; Soufflé Datalog rules compose them into cross-function findings; Z3 filters infeasible paths and emits SAT models; runtime range invariants from a handful of corpus seeds are folded in; and a second LLM agent synthesizes candidate crashing inputs that are validated by an ASan harness. The paper reports end-to-end rediscovery of eight CVE-class issues (including the CVSS-9.8 CVE-2023-38545 in curl 8.3.0) plus five memory-safety bugs on libarchive HEAD (four previously unreported), with upstream filings and merges.

Significance. If the per-function LLM facts prove sufficiently accurate and complete, the approach offers a practical, auditable alternative to heavyweight static analyzers by avoiding build requirements while retaining symbolic composition and SMT filtering. The concrete ASan-confirmed rediscoveries, new bug reports with rapid upstream acknowledgment, and crash-synthesis examples (e.g., 102-byte stb_vorbis input) demonstrate end-to-end utility and provide falsifiable artifacts. The explicit separation of LLM fact extraction from Datalog/SMT reasoning is a strength that supports auditability.

major comments (2)
  1. [Methodology / Evaluation] The central claim that LLM-derived facts are accurate and complete enough for correct Datalog composition and Z3 filtering rests on an unverified assumption. No precision, recall, or error-rate measurements are reported for the typed dataflow, aliasing, or range facts extracted by the LLM against manual ground truth on the evaluated codebases (stb, curl, libarchive, libxml2, FFmpeg slice). Without such an oracle or quantitative audit of the fact base, the reported ASan-confirmed findings could result from fortunate LLM outputs rather than reliable pipeline behavior (abstract; pipeline description).
  2. [Abstract / Results] The evaluation does not address the risk of post-hoc selection of libraries, functions, or corpus seeds. The abstract reports successes on a small set of named libraries but provides no counts of false positives, total queries attempted, or failure cases, making it difficult to assess the pipeline's overall reliability or generalizability.
minor comments (2)
  1. [Methodology] The description of the LLM prompt engineering, model choice, and temperature settings is minimal; expanding this would aid reproducibility of the fact-extraction step.
  2. [Pipeline description] Figure or table summarizing the exact Datalog rules and the Z3 encoding of the SAT models would clarify how the composition and filtering steps operate on the LLM facts.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive feedback emphasizing the need for quantitative validation of the LLM fact base and a more complete picture of evaluation outcomes. We address each major comment below and commit to revisions that directly respond to the concerns raised.

read point-by-point responses

  1. Referee: [Methodology / Evaluation] The central claim that LLM-derived facts are accurate and complete enough for correct Datalog composition and Z3 filtering rests on an unverified assumption. No precision, recall, or error-rate measurements are reported for the typed dataflow, aliasing, or range facts extracted by the LLM against manual ground truth on the evaluated codebases (stb, curl, libarchive, libxml2, FFmpeg slice). Without such an oracle or quantitative audit of the fact base, the reported ASan-confirmed findings could result from fortunate LLM outputs rather than reliable pipeline behavior (abstract; pipeline description).

    Authors: We agree that the absence of precision/recall metrics against manual ground truth leaves the reliability of the fact-extraction step less quantified than ideal. The manuscript's primary validation is end-to-end: ASan-confirmed rediscovery of eight CVEs (including CVE-2023-38545) plus five new bugs with upstream acceptance. This provides evidence that the composed facts were sufficient for the reported outcomes, but does not directly measure per-fact accuracy. In revision we will add an appendix containing a manual audit on a stratified sample of functions drawn from the evaluated codebases, reporting precision and recall for dataflow, aliasing, and range facts. This will be performed by the authors on a held-out subset and presented with inter-annotator agreement notes. revision: yes

  2. Referee: [Abstract / Results] The evaluation does not address the risk of post-hoc selection of libraries, functions, or corpus seeds. The abstract reports successes on a small set of named libraries but provides no counts of false positives, total queries attempted, or failure cases, making it difficult to assess the pipeline's overall reliability or generalizability.

    Authors: The libraries were chosen a priori as widely used open-source projects containing documented CVEs suitable for rediscovery experiments; the libarchive results were obtained on HEAD without prior knowledge of the specific bugs. Nevertheless, the manuscript reports only successful cases and omits aggregate statistics. We will revise the evaluation section to report: (i) total functions analyzed per library, (ii) total Datalog queries issued, (iii) number of findings before and after Z3 filtering, (iv) observed false-positive patterns (e.g., over-approximated aliasing), and (v) a brief discussion of failure modes encountered during development. These additions will be placed in the main evaluation section rather than an appendix. revision: yes

Circularity Check

0 steps flagged

No circularity: pipeline uses external tools and reports empirical results on public codebases

full rationale

The paper describes an end-to-end pipeline (LLM fact extraction per function, Soufflé Datalog composition, Z3 filtering, runtime invariants from seeds, and ASan-validated crash synthesis) without any mathematical derivations, fitted parameters renamed as predictions, or load-bearing self-citations. Claims rest on re-discovery of known CVEs and new bugs in public libraries (curl, libarchive, stb, etc.) using external components (Soufflé, Z3, ASan). No equations or steps reduce to the paper's own inputs by construction; the central claim remains independent.

Axiom & Free-Parameter Ledger

1 free parameters · 2 axioms · 0 invented entities

The system relies on standard external solvers and the assumption that LLM fact extraction is sufficiently reliable for the downstream composition step. No new physical constants or fitted global parameters are introduced in the abstract.

free parameters (1)
  • handful of corpus seeds
    A small number of example inputs used to derive likely range invariants that tighten the SMT problem; the exact count and selection method are not specified.
axioms (2)
  • domain assumption LLM can extract typed dataflow facts one function at a time that are accurate enough for cross-function composition
    Invoked in the description of the first pipeline stage; if false the entire fact base is unreliable.
  • standard math Datalog rules can correctly compose per-function facts into cross-function findings
    Standard assumption for Datalog-based static analysis; location is the Souffle rule mesh step.

pith-pipeline@v0.9.1-grok · 5936 in / 1671 out tokens · 19145 ms · 2026-06-28T18:36:48.883442+00:00 · methodology

0 comments
read the original abstract

Vulnerability discovery on C/C++ source asks the analyst to choose between heavyweight static analysers, which need a working build before a single query runs, and free-form LLMs, which read source readily but invent details and lose track of cross-function dataflow on real codebases. We present NeuroLog, an end-to-end build-free pipeline that assigns each layer the role it is uniquely good at: an LLM extracts typed dataflow facts one function at a time; a Souffle rule mesh composes those facts into cross-function findings; a Z3 post-pass filters infeasible findings and emits a SAT model for each survivor. To go beyond pure static reasoning we also fold in runtime evidence: likely range invariants from a handful of corpus seeds tighten the SMT problem at near-zero cost. A second LLM agent reads each SAT model and writes a Python program that produces a candidate crashing input, validated by an AddressSanitizer harness. Combining static-narrowing-SMT (Saturn, Pinpoint) and Datalog-with-SMT (Formulog) is prior art; new here are an LLM-derived fact base, a no-build pipeline, and the SAT model as an artifact (input to crash synthesis) rather than a yes/no verdict. Across stb, cJSON, libxml2, an FFmpeg demuxer slice, and curl 8.3.0, NeuroLog re-discovers eight CVE-class issues end-to-end, including the CVSS-9.8 SOCKS5 heap overflow CVE-2023-38545, each ASan-confirmed. On libarchive HEAD we surface five memory-safety bugs (four previously unreported) across the cpio reader and the XAR/WARC/7zip writers; all filed upstream, several fixes merged, with the cpio use-after-free acknowledged in seven hours. Extraction takes ~37 s and $0.005 on stb; crash synthesis turned a static finding into a 102-byte stb_vorbis crash in two LLM iterations (no fuzzer); a likely-invariant filter from three Matroska seeds eliminates 13.2% of the FFmpeg-demuxer feasible set.

Figures

Figures reproduced from arXiv: 2606.00669 by Sanjay Rawat.

Figure 1
Figure 1. Figure 1: Datalog derivation tree on the stb_vorbis CVE-2023-45676 region of Listing 1. Blue boxes are extracted facts (LLM smell pass + tree-sitter); grey boxes are catalog facts shipped with NeuroLog; orange boxes are derived relations the rule mesh produces. The bold top tuple is the report the analyst sees. Every step in the derivation is mechanically auditable and reproducible by re-running Soufflé on the same … view at source ↗
Figure 2
Figure 2. Figure 2: NeuroLog’s pipeline. Solid stages exchange artifacts sequentially; orange stages are the two LLM moments (per-function fact extraction, post-SMT crash synthesis); the dashed boxes are the Phase E precision passes that attach to the relevant stage boundaries. The arc from Harness back to Synth is the Phase C multi-shot retry loop. Crucially, no stage requires the target to be compiled; the only built artifa… view at source ↗
Figure 3
Figure 3. Figure 3: Producer split for the twelve-relation fact schema. The mechanical floor (blue) handles [PITH_FULL_IMAGE:figures/full_fig_p010_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Phase C multi-shot synthesis loop. The agent receives the SMT witness (the value the [PITH_FULL_IMAGE:figures/full_fig_p014_4.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

51 extracted references · 5 canonical work pages

  1. [1]

    Program analysis and specialization for the C programming language

    Lars Ole Andersen. Program analysis and specialization for the C programming language. InPh.D. Thesis, DIKU, University of Copenhagen, 1994

    1994

  2. [2]

    cpio reader: record_hardlink() UAF/double-free regression —free(le) leaves dangling pointer in cpio->links_head

    Anonymous. cpio reader: record_hardlink() UAF/double-free regression —free(le) leaves dangling pointer in cpio->links_head. https://github.com/libarchive/ libarchive/issues/3053, 2026. Filed 2026-05-20; acknowledged with fix PR #3055 in 7 hours, reporter credited as commit author

    2026

  3. [3]

    7zip writer: file_new() leaks file->utf16name on symlink utf-8 conversion failure

    Anonymous. 7zip writer: file_new() leaks file->utf16name on symlink utf-8 conversion failure. GitHub issue (URL pending: will be filled when filed), 2026

    2026

  4. [4]

    warcwriter: _warc_header()leaks archive_stringon _popul_ehdroverflow

    Anonymous. warcwriter: _warc_header()leaks archive_stringon _popul_ehdroverflow. GitHub issue (URL pending: will be filled when filed), 2026

    2026

  5. [5]

    xar reader: file_free() misses archive_string_free for fflags_text (heap leak)

    Anonymous. xar reader: file_free() misses archive_string_free for fflags_text (heap leak). https://github.com/libarchive/libarchive/issues/3058, 2026. Filed 2026-05-21; acknowledged with fix PR #3060 within∼18 hours

    2026

  6. [6]

    xar writer: make_fflags_entry() oob read into .rodata past string- literal null terminator

    Anonymous. xar writer: make_fflags_entry() oob read into .rodata past string- literal null terminator. https://github.com/libarchive/libarchive/issues/3059,

  7. [7]

    Filed 2026-05-21; concurrent with maintainer’s in-flight fix PR #3041 (GHSA-wfvr-54j8-47r9)

    2026

  8. [8]

    QL: Object- oriented queries on relational data

    Pavel Avgustinov, Oege de Moor, Michael Peyton Jones, and Max Schäfer. QL: Object- oriented queries on relational data. InEuropean Conference on Object-Oriented Programming (ECOOP), 2016. 24

    2016

  9. [9]

    stb single-file public-domain libraries for C/C++.https://github.com/ nothings/stb, 2024

    Sean Barrett. stb single-file public-domain libraries for C/C++.https://github.com/ nothings/stb, 2024

    2024

  10. [10]

    Formulog: Datalog for SMT- based static analysis.Proceedings of the ACM on Programming Languages (PACMPL), OOPSLA, 4(OOPSLA), 2020

    Aaron Bembenek, Michael Greenberg, and Stephen Chong. Formulog: Datalog for SMT- based static analysis.Proceedings of the ACM on Programming Languages (PACMPL), OOPSLA, 4(OOPSLA), 2020. arXiv:2009.08361

    work page arXiv 2020

  11. [11]

    Making Formulog fast: An argument for unconventional Datalog evaluation.Proceedings of the ACM on Programming Languages (PACMPL), OOPSLA2, 8(OOPSLA2), 2024

    Aaron Bembenek, Michael Greenberg, and Stephen Chong. Making Formulog fast: An argument for unconventional Datalog evaluation.Proceedings of the ACM on Programming Languages (PACMPL), OOPSLA2, 8(OOPSLA2), 2024. arXiv:2408.14017

    work page arXiv 2024

  12. [12]

    Strictly declarative specification of sophis- ticated points-to analyses

    Martin Bravenboer and Yannis Smaragdakis. Strictly declarative specification of sophis- ticated points-to analyses. InObject-Oriented Programming, Systems, Languages, and Applications (OOPSLA), 2009

    2009

  13. [13]

    Tree-sitter: An incremental parsing system for programming tools

    Max Brunsfeld et al. Tree-sitter: An incremental parsing system for programming tools. https://tree-sitter.github.io/tree-sitter/, 2024

    2024

  14. [14]

    Cristian Cadar, Daniel Dunbar, and Dawson R. Engler. KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. InOperating Systems Design and Implementation (OSDI), 2008

    2008

  15. [15]

    Fink, and Manu Sridharan

    Satish Chandra, Stephen J. Fink, and Manu Sridharan. Snugglebug: A powerful approach to weakest preconditions. InProgramming Language Design and Implementation (PLDI), 2009

    2009

  16. [16]

    SOCKS4a long-username/hostname heap overflow (strcpy joint-bound check), hackerone disclosure

    curl project. SOCKS4a long-username/hostname heap overflow (strcpy joint-bound check), hackerone disclosure. https://github.com/curl/curl/commit/01057d6161, 2023. Patch 01057d6161, curl 8.4.0

    2023

  17. [17]

    Z3: An efficient SMT solver

    Leonardo de Moura and Nikolaj Bjørner. Z3: An efficient SMT solver. InTools and Algorithms for the Construction and Analysis of Systems (TACAS), 2008

    2008

  18. [18]

    Ernst, Jeff H

    Michael D. Ernst, Jeff H. Perkins, Philip J. Guo, Stephen McCamant, Carlos Pacheco, Matthew S. Tschantz, and Chen Xiao. The Daikon system for dynamic detection of likely invariants.Science of Computer Programming, 69(1–3):35–45, 2007

    2007

  19. [19]

    cJSON: An ultralightweight JSON parser in ANSI C

    Dave Gamble and contributors. cJSON: An ultralightweight JSON parser in ANSI C. https://github.com/DaveGamble/cJSON, 2024

    2024

  20. [20]

    CVE-2023-45676: Integer overflow leading to heap-based buffer overflow in stb_vorbis comment-parsing path (GHSL-2023-166).https://nvd.nist.gov/ vuln/detail/CVE-2023-45676, 2023

    GitHub Security Lab. CVE-2023-45676: Integer overflow leading to heap-based buffer overflow in stb_vorbis comment-parsing path (GHSL-2023-166).https://nvd.nist.gov/ vuln/detail/CVE-2023-45676, 2023

    2023

  21. [21]

    CVE-2023-45681: Integer overflow in stb_vorbis comment-list alloca- tion (GHSL-2023-171).https://nvd.nist.gov/vuln/detail/CVE-2023-45681, 2023

    GitHub Security Lab. CVE-2023-45681: Integer overflow in stb_vorbis comment-list alloca- tion (GHSL-2023-171).https://nvd.nist.gov/vuln/detail/CVE-2023-45681, 2023

    2023

  22. [22]

    Levin, and David Molnar

    Patrice Godefroid, Michael Y. Levin, and David Molnar. Automated whitebox fuzz testing. InNetwork and Distributed System Security (NDSS), 2008

    2008

  23. [23]

    Magma: A Ground-Truth Fuzzing Benchmark,

    Ahmad Hazimeh, Adrian Herrera, and Mathias Payer. Magma: A ground-truth fuzzing benchmark. InProceedings of the ACM on Measurement and Analysis of Computing Systems (POMACS), 2020. doi: 10.1145/3428334

    work page doi:10.1145/3428334 2020

  24. [24]

    Soufflé: On synthesis of pro- gram analyzers

    Herbert Jordan, Bernhard Scholz, and Pavle Subotić. Soufflé: On synthesis of pro- gram analyzers. InComputer Aided Verification (CAV), 2016. Project home: https: //souffle-lang.github.io/. 25

    2016

  25. [25]

    Failure sketching: A technique for automated root cause diagnosis of in-production failures

    Baris Kasikci, Benjamin Schubert, Cristiano Pereira, Gilles Pokam, and George Candea. Failure sketching: A technique for automated root cause diagnosis of in-production failures. InACM Symposium on Operating Systems Principles (SOSP), 2015

    2015

  26. [26]

    libarchive: Multi-format archive and compression library

    Tim Kientzle and contributors. libarchive: Multi-format archive and compression library. https://github.com/libarchive/libarchive, 2026

    2026

  27. [27]

    Llm-assisted static analysis for detecting security vulnerabilities,

    Ziyang Li, Saikat Dutta, and Mayur Naik. IRIS: LLM-assisted static analysis for detecting security vulnerabilities. arXiv:2405.17238, 2024.https://arxiv.org/abs/2405.17238

    work page arXiv 2024

  28. [28]

    libFuzzer: A library for coverage-guided fuzz testing.https://llvm.org/ docs/LibFuzzer.html, 2024

    LLVM Project. libFuzzer: A library for coverage-guided fuzz testing.https://llvm.org/ docs/LibFuzzer.html, 2024

    2024

  29. [29]

    CVE-2023-38545: SOCKS5 heap buffer overflow in curl.https://nvd.nist.gov/ vuln/detail/CVE-2023-38545, 2023

    NVD. CVE-2023-38545: SOCKS5 heap buffer overflow in curl.https://nvd.nist.gov/ vuln/detail/CVE-2023-38545, 2023

    2023

  30. [30]

    CVE-2023-53154: Heap buffer over-read in cJSON string parsing.https://nvd

    NVD. CVE-2023-53154: Heap buffer over-read in cJSON string parsing.https://nvd. nist.gov/vuln/detail/CVE-2023-53154, 2023

    2023

  31. [31]

    CVE-2025-10148: Predictable per-connection mask key in curl WebSocket.https: //nvd.nist.gov/vuln/detail/CVE-2025-10148, 2025

    NVD. CVE-2025-10148: Predictable per-connection mask key in curl WebSocket.https: //nvd.nist.gov/vuln/detail/CVE-2025-10148, 2025

    2025

  32. [32]

    CVE-2025-57052: Out-of-bounds access in cJSON json-pointer handling.https: //nvd.nist.gov/vuln/detail/CVE-2025-57052, 2025

    NVD. CVE-2025-57052: Out-of-bounds access in cJSON json-pointer handling.https: //nvd.nist.gov/vuln/detail/CVE-2025-57052, 2025

    2025

  33. [33]

    CVE-2025-6021: Integer overflow in libxml2xmlBuildQName

    NVD. CVE-2025-6021: Integer overflow in libxml2xmlBuildQName. https://nvd.nist. gov/vuln/detail/CVE-2025-6021, 2025

    2025

  34. [34]

    Precise interprocedural dataflow analysis via graph reachability

    Thomas Reps, Susan Horwitz, and Mooly Sagiv. Precise interprocedural dataflow analysis via graph reachability. InPrinciples of Programming Languages (POPL), 1995

    1995

  35. [35]

    Top score on the wrong exam: On benchmarking in machine learning for vulnerability detection.Proc

    Niklas Risse, Jing Liu, and Marcel Böhme. Top score on the wrong exam: On benchmarking in machine learning for vulnerability detection.Proc. ACM Softw. Eng., 2(ISSTA):388–410,

  36. [36]

    arXiv:2408.12986

    doi: 10.1145/3728887. arXiv:2408.12986

    work page doi:10.1145/3728887

  37. [37]

    Using likely invari- ants for automated software fault localization

    Swarup Kumar Sahoo, John Criswell, Chase Geigle, and Vikram Adve. Using likely invari- ants for automated software fault localization. InArchitectural Support for Programming Languages and Operating Systems (ASPLOS), 2013

    2013

  38. [38]

    Ad- dressSanitizer: A fast address sanity checker

    Konstantin Serebryany, Derek Bruening, Alexander Potapenko, and Dmitriy Vyukov. Ad- dressSanitizer: A fast address sanity checker. https://www.usenix.org/conference/ atc12/technical-sessions/presentation/serebryany, 2012

    2012

  39. [39]

    Pinpoint: Fast and precise sparse value flow analysis for million lines of code

    Qingkai Shi, Xiao Xiao, Rongxin Wu, Jinguo Zhou, Gang Fan, and Charles Zhang. Pinpoint: Fast and precise sparse value flow analysis for million lines of code. InProgramming Language Design and Implementation (PLDI), 2018

    2018

  40. [40]

    and the Joern community

    ShiftLeft, Inc. and the Joern community. Joern: Open-source code analysis platform for C/C++, java, javascript, and others.https://joern.io/, 2024. C/C++ frontend (c2cpg) parses source directly;gccis used only optionally for system-header auto-discovery

    2024

  41. [41]

    SoK: (state of) the art of war: Offensive techniques in binary analysis

    Yan Shoshitaishvili, Ruoyu Wang, Christopher Salls, Nick Stephens, Mario Polino, Andrew Dutcher, John Grosen, Siji Feng, Christophe Hauser, Christopher Kruegel, and Giovanni Vigna. SoK: (state of) the art of war: Offensive techniques in binary analysis. InIEEE Symposium on Security and Privacy (S&P), 2016. 26

    2016

  42. [42]

    xar: Fix writer oob accesses with fflags (resolves GHSA-wfvr-54j8-47r9)

    Tobias Stoeckmann. xar: Fix writer oob accesses with fflags (resolves GHSA-wfvr-54j8-47r9). https://github.com/libarchive/libarchive/pull/3041,

  43. [43]

    Opened 2026-05-16; concurrent in-flight fix for the same XAR-writer OOB read site we independently identified two days later

    2026

  44. [44]

    SVF: Interprocedural static value-flow analysis in LLVM

    Yulei Sui and Jingling Xue. SVF: Interprocedural static value-flow analysis in LLVM. In International Conference on Compiler Construction (CC), 2016

    2016

  45. [45]

    FFmpeg: A complete, cross-platform solution to record, convert and stream audio and video.https://ffmpeg.org/, 2024

    The FFmpeg Project. FFmpeg: A complete, cross-platform solution to record, convert and stream audio and video.https://ffmpeg.org/, 2024

    2024

  46. [46]

    Cottontail: Large language model-driven concolic execution for highly structured test input generation

    Haoxin Tu, Seongmin Lee, Yuxian Li, Peng Chen, Lingxiao Jiang, and Marcel Böhme. Cottontail: Large language model-driven concolic execution for highly structured test input generation. InIEEE Symposium on Security and Privacy (S&P), 2026

    2026

  47. [47]

    libxml2: The XML C parser and toolkit of Gnome

    Daniel Veillard and contributors. libxml2: The XML C parser and toolkit of Gnome. https://gitlab.gnome.org/GNOME/libxml2, 2024

    2024

  48. [48]

    John Whaley and Monica S. Lam. Cloning-based context-sensitive pointer alias analysis using binary decision diagrams. InProgramming Language Design and Implementation (PLDI), 2004

    2004

  49. [49]

    Saturn: A SAT-based tool for bug detection

    Yichen Xie and Alex Aiken. Saturn: A SAT-based tool for bug detection. InComputer Aided Verification (CAV), 2005

    2005

  50. [50]

    Saturn: A scalable framework for error detection using Boolean satisfiability.ACM Transactions on Programming Languages and Systems (TOPLAS), 29 (3), 2007

    Yichen Xie and Alex Aiken. Saturn: A scalable framework for error detection using Boolean satisfiability.ACM Transactions on Programming Languages and Systems (TOPLAS), 29 (3), 2007

    2007

  51. [51]

    f/i” is feasible/infeasible. “B flips

    Fabian Yamaguchi, Nico Golde, Daniel Arp, and Konrad Rieck. Modeling and discovering vulnerabilities with code property graphs. InIEEE Symposium on Security and Privacy (S&P), 2014. A The NeuroLog rule mesh This appendix lists every output relation the rule mesh produces, grouped by the bug family it targets. The relations are the shared interface between...

    2014