Pith. sign in

REVIEW 1 major objections 6 minor 23 references

A 519-line translation guide lifts LLM kernel specs from 55% to 97%

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 · glm-5.2

2026-07-05 01:55 UTC pith:AY5OEIPI

load-bearing objection Solid empirical result with a real generalization gap that needs addressing before publication. the 1 major comments →

arxiv 2605.23931 v1 pith:AY5OEIPI submitted 2026-04-22 cs.AI cs.PLcs.SE

BODHI: Precise OS Kernel Specification Inference

Zhiming Chang , Ziyang Li This is my paper
classification cs.AI cs.PLcs.SE
keywords formal specification generationLLM promptingdomain knowledge injectionOS kernel verificationZ3 SMT solvertranslation guidestructured chain-of-thoughtOSV-Bench
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 claims that the bottleneck in using large language models to generate formal specifications for operating system kernels is not reasoning ability but domain-specific translation knowledge — the kind of knowledge that tells you IOMMU page table entries use byte addressing while x86 entries use shifted page-frame numbers, or that Z3 map fields use parentheses for reads but brackets for writes. The authors construct a 519-line structured reference document, called a translation guide, covering 15 categories of C-to-Python/Z3 translation patterns derived from analyzing the failure modes of a mid-tier model on the OSV-Bench benchmark. When this guide is inserted into the prompt immediately before the target task, every one of nine models from six providers improves, with gains from +11 to +32 percentage points. The best configuration reaches 96.73% Pass@1, up from a previous best of 55.10%. The guide organizes translation knowledge by separation of concerns: pre-condition extraction (negating C error checks into Z3 guards) and post-condition generation (mapping C state mutations to Z3 field assignments) are treated as distinct categories, reducing cross-contamination errors where models mix the two. The paper argues that the largest gains accrue to mid-tier models that have enough instruction-following capability to parse and apply structured reference material but lack the specialized domain knowledge themselves, pointing to a productive division of labor between human domain experts who construct the guide and LLMs that apply it at scale.

Core claim

The central discovery is that formal specification generation by LLMs fails primarily due to missing domain-specific translation knowledge, not insufficient reasoning, and that this knowledge can be effectively injected as a structured reference document placed at the end of the prompt. The translation guide — a 519-line, 15-category reference covering syntax conventions, domain-specific formulas (PTE formulas, reference counting, IPC state machines), and completeness patterns — acts as a domain textbook that the model consults during generation. The guide was constructed by running a mid-tier model on the benchmark, classifying its failures, and codifying the oracle specification patterns (

What carries the argument

The translation guide is the central object. It is a structured reference document with 15 categories organized in three tiers: (1) syntax-level patterns ensuring the specification can be constructed (template structure, pre-condition negation, post-condition patterns, map field read/write syntax, operator rules, constant prefixes); (2) domain-specific semantic patterns (PTE formulas distinguishing x86 from IOMMU addressing, shadow metadata fields, reference counting semantics, TLB flush differences, state pointer names, field name mapping); and (3) completeness patterns for complex system calls (C helper function expansion, available helper inventory, IPC state-machine patterns). The guide~

Load-bearing premise

The translation guide was constructed by analyzing failures of Claude Haiku 4.5 on the same 245-task OSV-Bench evaluation set, and its patterns were derived from inspecting the oracle specifications for those same tasks. If the guide encodes benchmark-specific patterns rather than transferable domain knowledge, the gains would not generalize to other OS kernels or verification targets.

What would settle it

Apply BODHI's methodology — failure analysis followed by structured guide construction — to a different formal verification benchmark (e.g., a different OS kernel or a different specification language) and check whether comparable gains are achieved without reconstructing the guide from scratch.

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

If this is right

  • If the approach generalizes, domain-specific translation guides could become a standard component of prompts for formal artifact generation in other verification domains (hardware, compilers, distributed systems), reducing the expertise barrier to formal verification.
  • The finding that mid-tier models benefit most suggests a practical strategy: pair cheaper models with high-quality domain reference material rather than relying solely on frontier models, potentially reducing the cost of specification generation.
  • The separation-of-concerns principle could be extended to multi-stage generation where pre-conditions and post-conditions are generated in separate LLM calls, which the authors propose as future work.
  • The asymmetry between actionable syntax error feedback and opaque semantic error counterexamples from Z3 suggests that automated repair loops would be most effective for syntax failures, where error messages are precise and machine-readable.

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

1 major / 6 minor

Summary. The paper proposes BODHI, a domain-knowledge prompting method that augments standard few-shot prompts with a 519-line structured C-to-Python/Z3 translation guide covering 15 categories of translation patterns. The guide is inserted between few-shot examples and the target task in the prompt. Evaluated on OSV-Bench (245 specification generation tasks from the Hyperkernel OS kernel), BODHI improves all nine models tested (from six providers), with gains from +11% to +32% Pass@1, reaching 96.73% with Claude Opus 4.6, substantially exceeding the previous best of 55.10%. The experimental design is well-controlled: same tasks, same evaluation protocol, only variable is the guide. The paper includes detailed error analysis (syntax vs. semantic, per-syscall breakdown) and qualitative case studies illustrating how the guide resolves specific failure modes.

Significance. The paper addresses a genuine bottleneck in formal OS kernel verification: specification writing. The reported improvement from 55.10% to 96.73% Pass@1 is substantial. Strengths include: (1) a controlled experimental design with nine models from six providers, isolated per-task API calls, and greedy decoding for reproducibility; (2) Z3 verification in the Docker environment providing a rigorous, binary correctness signal; (3) detailed error analysis decomposing failures into syntax/semantic subcategories; (4) qualitative case studies (§IV.F) that concretely illustrate the guide's mechanism of action. The methodology of systematic failure analysis followed by structured knowledge injection is clearly described and could plausibly transfer to other verification domains. However, the significance of the results is substantially undermined by the train-test overlap concern (see Major Comments).

major comments (1)
  1. §III.B and §VI.A: The translation guide was constructed by (1) running Claude Haiku 4.5 on the 245 OSV-Bench tasks, (2) classifying its 122 failures, and (3) inspecting oracle specifications of those same tasks to extract patterns (§III.B: 'identify recurring patterns in the ground truth oracle specifications'). The guide is then evaluated on those same 245 tasks. This is the single most load-bearing concern: without a held-out split, the reported gains cannot be distinguished from benchmark overfitting. The paper's mitigations in §VI.A are insufficient — claiming the guide contains 'only general translation rules' is an assertion, not evidence, and the fact that Devstral 2 (a different provider) shows the largest gain does not address the concern, since all models are tested on the same tasks the guide was built from. Some categories appear to encode Hyperkernel-specific details that pl
minor comments (6)
  1. §IV.A: The paper reports single-run results rather than the 3-run average used in the original OSV-Bench evaluation. While greedy decoding is mostly deterministic, the paper should note which models exhibited non-determinism and how much variance was observed.
  2. TABLE II: The DeepSeek-R1 baseline (26.53%) is substantially lower than the published result (40.00% [1]). The footnote attributes this to 'API version differences and single-run evaluation' but this large gap warrants more investigation or at least acknowledgment that it complicates comparison with published baselines.
  3. §IV.B: The claim that BODHI's effect is 'comparable to or greater than a full model generation upgrade' (comparing Sonnet 3.5 → Sonnet 4 baseline gain of +16.3% vs. Sonnet 4 + BODHI gain of +13.9%) is somewhat misleading since the baseline comparison involves different model versions while BODHI is an additive prompt modification.
  4. Fig. 5: The y-axis starts at 0 but the dashed red line at 55.10% could be more prominently labeled. Consider adding the numerical gain above each model pair for readability.
  5. §III.B, last paragraph: 'It includes no task-specific code or complete solutions for any system call' — this claim would be strengthened by making the full guide available as a supplementary artifact for inspection.
  6. TABLE III: The sys_lseek regression (5/5 → 4/5) is attributed to a Z3 API version mismatch (z3.SLT not available in v4.5.0). This suggests the guide may have introduced an incorrect pattern; consider noting whether this is a guide error or a model application error.

Simulated Author's Rebuttal

3 responses · 0 unresolved

The referee raises one major concern: the translation guide was constructed by analyzing failures on the same 245 OSV-Bench tasks on which it is evaluated, creating a potential train-test overlap that could inflate results. We agree this is the most important methodological concern and will address it with a held-out split experiment in the revision. We also provide substantive arguments for why the current evidence already substantially mitigates the overfitting concern.

read point-by-point responses

  1. Referee: §III.B and §VI.A: The translation guide was constructed by (1) running Claude Haiku 4.5 on the 245 OSV-Bench tasks, (2) classifying its 122 failures, and (3) inspecting oracle specifications of those same tasks to extract patterns. The guide is then evaluated on those same 245 tasks. Without a held-out split, the reported gains cannot be distinguished from benchmark overfitting.

    Authors: We agree that the absence of a held-out split is a legitimate methodological gap and will address it in the revision. Specifically, we will construct the guide using only failures from a randomly selected subset of the 245 tasks (e.g., 120 tasks) and then evaluate BODHI on the remaining held-out tasks. We will report results on both the development and held-out splits for all nine models. We expect the held-out performance to remain substantially above baseline for the following reasons, which we will verify empirically: (1) The guide encodes general translation rules, not task-specific solutions. For example, Category 4 teaches that Z3 map fields use parentheses for reads but brackets for writes — this is a property of the Z3 Python API, not of any particular system call. Category 7 distinguishes x86 PTE formulas (shifted page-frame numbers) from IOMMU PTE formulas (direct byte addressing) — this is a hardware architecture fact, not a pattern specific to any individual task. The guide contains no complete specifications for any of the 245 tasks. (2) The guide was developed using Claude Haiku 4.5's failures, yet the largest gain is observed on Devstral 2 (+31.8%), a model from a different provider that was not involved in guide development. If the guide were overfit to Haiku's specific failure modes, we would expect the largest gains on Haiku itself. Instead, the guide improves all nine models from six providers, including models with entirely different architectures (MoE, reasoning, dense). (3) The 15 categories cover structural translation patterns (pre-condition negation, post-condition assignment, field naming conventions, operator overloading rules) that are inherent to the C-to-Z3 translation task, not to specific test cases. A held-out task requiring the same C→Z revision: no

  2. Referee: The paper's mitigations in §VI.A are insufficient — claiming the guide contains 'only general translation rules' is an assertion, not evidence, and the fact that Devstral 2 (a different provider) shows the largest gain does not address the concern, since all models are tested on the same tasks the guide was built from.

    Authors: We accept this criticism. The claim that the guide contains only general rules is currently supported by description rather than by experimental evidence. The held-out split experiment described above will convert this assertion into testable evidence. We will also add to the revision a concrete analysis showing that each of the 15 guide categories applies to multiple system calls (not just the ones whose failures motivated the category), demonstrating that the patterns are reusable across tasks rather than memorized from specific oracle specifications. Additionally, we will release the full 519-line guide as supplementary material so reviewers can directly inspect whether any category encodes task-specific information. We believe transparency is the strongest response to this concern: if the guide were an answer key, this would be immediately apparent upon inspection. revision: no

  3. Referee: Some categories appear to encode Hyperkernel-specific details that plausibly overlap with test tasks.

    Authors: This is partially correct and we will be transparent about it in the revision. Categories 7 (PTE formulas), 8 (shadow metadata), 9 (reference counting), 10 (TLB flush), and 15 (IPC state machines) do encode Hyperkernel-specific domain knowledge. However, these are general patterns that apply across multiple system calls within the Hyperkernel codebase, not solutions to specific tasks. For example, the IOMMU PTE formula (byte addressing instead of page-frame shifting) applies to all IOMMU-related system calls (sys_alloc_iommu_pt, sys_alloc_iommu_pdpt, sys_reclaim_iommu_frame, etc.), and the IPC implication pattern applies to all three IPC system calls (call_proc, send_proc, reply_wait_proc). The distinction we draw is between domain knowledge (which is inherently specific to the verification target) and task-specific solutions (which would constitute overfitting). The guide encodes the former, not the latter. That said, we acknowledge that domain-specific knowledge injection will always have some degree of coupling to the target codebase, and we will add a clearer discussion of this limitation in the revision. The held-out experiment will quantify how much of the gain is attributable to genuinely reusable patterns versus proximity to specific development-set tasks. revision: no

Circularity Check

1 steps flagged

Translation guide was constructed by inspecting oracle specs of the same 245 evaluation tasks; gains are partly forced by this fit, but the guide contains general patterns and evaluation uses independent Z3 verification, so the reduction is partial rather than definitional.

specific steps
  1. fitted input called prediction [§III.B (Translation Guide Design), lines describing construction process; §VI.A (Internal Validity)]
    "It was constructed through an iterative process: (1) run baseline prompting on a subset of tasks, (2) classify failures into error types, (3) identify recurring patterns in the ground truth oracle specifications that address each error type, and (4) codify these patterns into structured guide categories. [...] We used Claude Haiku 4.5 as the development model to maximize failure coverage during guide construction. The Claude Haiku 4.5 baseline achieved 50.20% Pass@1 (123/245), producing 49 syntax errors and 73 semantic errors across 122 failed tasks spanning 30 of the 49 system calls. [...] A "

    The guide's 15 categories were derived by (a) running a model on the 245 OSV-Bench tasks, (b) classifying its 122 failures, and (c) inspecting the oracle specifications of those same tasks to extract patterns. The guide is then evaluated on those same 245 tasks. This is a train-test overlap: the guide was fitted to the evaluation set. Some categories appear to encode benchmark-specific detail (Category 7: '7 mapping variants'; Category 11: '6_ptr_to_int field exact names'), which could function as partial answer keys. The paper acknowledges this in §VI.A: 'the guide patterns were derived from inspecting oracle specifications.' However, the reduction is partial, not definitional: the guide contains general translation rules (e.g., 'IOMMU PTEs use byte addressing'), not complete task-level答案

full rationale

The paper's central claim—that BODHI improves specification generation—is not circular by construction. The guide does not contain task-specific answers, and evaluation uses independent Z3 formal verification (behavioral equivalence checking against compiled LLVM IR), which cannot be gamed by memorizing patterns. However, the guide was constructed by inspecting oracle specifications of the same 245 tasks it is evaluated on, with no held-out split. This constitutes a partial 'fitted input called prediction' pattern: the 15 categories were selected to address failure modes on this specific benchmark, and some categories (notably Category 7's '7 mapping variants' and Category 11's exact field names) may encode enough benchmark-specific detail to partially function as answer keys. The paper acknowledges this concern in §VI.A and offers mitigations (general patterns only, cross-model generalization to Devstral 2), but these are assertions rather than controlled evidence. The concern is about overfitting/contamination rather than definitional circularity—the guide is not equivalent to the test answers by construction, and the Z3 verifier provides an independent correctness check. Score 3 reflects this partial, non-definitional circularity.

Axiom & Free-Parameter Ledger

4 free parameters · 4 axioms · 0 invented entities

The paper introduces no new formal entities, particles, forces, dimensions, or mathematical objects. The translation guide is a hand-crafted artifact, not a postulated entity. The free parameters are design choices (guide content, placement, development model) rather than numeric fitted constants. The key axioms are inherited from OSV-Bench (Z3 as oracle) and transformer attention literature (recency effect). The most paper-specific axiom is that the guide encodes general rules rather than benchmark-specific solutions.

free parameters (4)
  • Translation guide content (15 categories, 519 lines) = 519 lines covering 15 categories derived from 122 failures of Claude Haiku 4.5 on OSV-Bench
    The guide's categories and content were selected based on failure analysis of one model on the evaluation set. While not a numeric parameter, it is a hand-crafted artifact tuned to the benchmark.
  • Guide placement (after few-shot examples, before target task) = Position: between examples and target
    Chosen to leverage recency effect in transformer attention (§III.A). This is a design choice justified by prior work [11] but not ablated against alternative placements.
  • Development model (Claude Haiku 4.5) = Claude Haiku 4.5
    Selected to maximize failure coverage during guide construction (§III.B). The choice of development model influences which error patterns the guide addresses.
  • Few-shot example count = 5
    Inherited from OSV-Bench protocol [1], not introduced by this paper, but affects all results.
axioms (4)
  • domain assumption Z3 verification (behavioral equivalence check via symbolic execution) is a correct oracle for specification quality.
    The entire evaluation depends on Z3's equivalence check (Eq. 2) being a valid correctness criterion. This is inherited from OSV-Bench [1] and Hyperkernel [7], where it is well-established.
  • domain assumption Greedy decoding (temperature 0.0) produces deterministic results that represent model capability without sampling variance.
    §IV.A: 'with greedy decoding, repeated runs are deterministic for most providers.' This justifies single-run evaluation but is not verified empirically in the paper.
  • ad hoc to paper The translation guide encodes general domain rules, not task-specific solutions for OSV-Bench.
    §III.B and §VI.A: The paper claims the guide 'contains only general translation rules and illustrative patterns derived from the oracle specifications' and 'includes no task-specific code or complete solutions.' This is the key assumption separating legitimate knowledge injection from benchmark overfitting.
  • domain assumption Recency effect in transformer attention makes guide placement after examples and before target task optimal.
    §III.A invokes [11] to justify guide placement. The paper does not ablate alternative placements, so this assumption is untested within the paper.

pith-pipeline@v1.1.0-glm · 18827 in / 3465 out tokens · 321656 ms · 2026-07-05T01:55:25.345288+00:00 · methodology

0 comments
read the original abstract

The formal verification of operating system kernels requires precise specifications that capture the intended behavior of system calls. Writing these specifications manually demands deep domain expertise, motivating the use of large language models (LLMs) to automate the process. However, in OSV-Bench, a benchmark of 245 specification generation tasks derived from the Hyperkernel OS kernel, the best reported Pass@1 is 55.10%. We propose a domain knowledge prompting method (BODHI), which augments the standard few-shot prompt with a structured C-to-Python translation guide covering 15 categories of domain-specific translation patterns. Inspired by Structured Chain-of-Thought (SCoT) prompting, the guide organizes translation by separation of concerns, addressing pre-condition extraction and post-condition generation as distinct categories. Evaluated on nine models from six providers (Anthropic, Mistral, Amazon, DeepSeek, Meta, Alibaba), covering dense, mixture-of-experts and reasoning architectures, BODHI improves every model tested, with gains ranging from +11% to +32%. The best configuration (Claude Opus 4.6 + BODHI) reaches 96.73% Pass@1. BODHI reduces both syntax and semantic errors, with the strongest effect on models that have sufficient instruction-following capability to utilize structured reference material. These results demonstrate that domain knowledge injection is a model-agnostic technique that substantially bridges the gap between general-purpose code generation and formal specification synthesis.

Figures

Figures reproduced from arXiv: 2605.23931 by Zhiming Chang, Ziyang Li.

Figure 1
Figure 1. Figure 1: Hyperkernel verification pipeline. The C implementa [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: The BODHI prompting pipeline. The prompt (left) contains five components; the [PITH_FULL_IMAGE:figures/full_fig_p003_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Excerpts from two translation guide categories. [PITH_FULL_IMAGE:figures/full_fig_p005_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Separation of concerns in the C-to-Z3 translation ( [PITH_FULL_IMAGE:figures/full_fig_p006_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Pass@1 on OSV-Bench across nine models from six providers, sorted by baseline performance. Each pair compares [PITH_FULL_IMAGE:figures/full_fig_p006_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Error distribution as nested donut charts for three representative models (weak/mid/strong). Inner ring: pass/syntax/se [PITH_FULL_IMAGE:figures/full_fig_p007_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

23 extracted references · 23 canonical work pages · 3 internal anchors

  1. [1]

    OSVBench: Benchmarking LLMs on specification generation tasks for operating system verification,

    S. Li, J. Jiang, T. Zhao, and J. Shen, “OSVBench: Benchmarking LLMs on specification generation tasks for operating system verification,” arXiv preprint arXiv:2504.20964, 2025

    work page arXiv 2025

  2. [2]

    Structured chain-of-thought prompting for code generation,

    J. Li, G. Li, Y . Li, and Z. Jin, “Structured chain-of-thought prompting for code generation,”arXiv preprint arXiv:2305.06599, 2023

    work page arXiv 2023

  3. [3]

    A survey of automated techniques for formal software verification,

    V . D’silva, D. Kroening, and G. Weissenbacher, “A survey of automated techniques for formal software verification,”IEEE Trans. Comput.-Aided Design Integr. Circuits Syst., vol. 27, no. 7, pp. 1165–1178, 2008

    work page 2008

  4. [4]

    seL4: Formal verification of an OS kernel,

    G. Klein, K. Elphinstone, G. Heiser, J. Andronick, D. Cock, P. Derrin, D. Elkaduwe, K. Engelhardt, R. Kolanski, M. Norrish, T. Sewell, H. Tuch, and S. Winwood, “seL4: Formal verification of an OS kernel,” inProc. ACM SIGOPS 22nd Symp. Operating Systems Principles, 2009, pp. 207–220

    work page 2009

  5. [5]

    Program Synthesis with Large Language Models

    J. Austin, A. Odena, M. Nye, M. Bosma, H. Michalewski, D. Dohan, E. Jiang, C. Cai, M. Terry, Q. Le, and C. Sutton, “Program synthesis with large language models,”arXiv preprint arXiv:2108.07732, 2021

    work page internal anchor Pith review Pith/arXiv arXiv 2021

  6. [6]

    A Survey on Large Language Models for Code Generation

    J. Jiang, F. Wang, J. Shen, S. Kim, and S. Kim, “A survey on large language models for code generation,”arXiv preprint arXiv:2406.00515, 2024

    work page internal anchor Pith review Pith/arXiv arXiv 2024

  7. [7]

    Hyperkernel: Push-button verification of an OS kernel,

    L. Nelson, H. Sigurbjarnarson, K. Zhang, D. Johnson, J. Bornholt, E. Torlak, and X. Wang, “Hyperkernel: Push-button verification of an OS kernel,” inProc. 26th Symp. Operating Systems Principles (SOSP), 2017, pp. 252–269

    work page 2017

  8. [8]

    Z3: An efficient SMT solver,

    L. D. Moura and N. Bjørner, “Z3: An efficient SMT solver,” inProc. Int. Conf. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2008, pp. 337–340

    work page 2008

  9. [9]

    LLVM: A compilation framework for lifelong program analysis & transformation,

    C. Lattner and V . Adve, “LLVM: A compilation framework for lifelong program analysis & transformation,” inProc. Int. Symp. Code Genera- tion and Optimization (CGO), 2004, pp. 75–86

    work page 2004

  10. [10]

    Chain-of-thought prompting elicits reasoning in large language models,

    J. Wei, X. Wang, D. Schuurmans, M. Bosma, B. Ichter, F. Xia, E. Chi, Q. Le, and D. Zhou, “Chain-of-thought prompting elicits reasoning in large language models,” inAdvances in Neural Information Processing Systems, vol. 35, 2022

    work page 2022

  11. [11]

    Lost in the middle: How language models use long contexts,

    N. F. Liu, K. Lin, J. Hewitt, A. Paranjape, M. Bevilacqua, F. Petroni, and P. Liang, “Lost in the middle: How language models use long contexts,” Trans. Assoc. Comput. Linguist., vol. 12, pp. 157–173, 2024

    work page 2024

  12. [12]

    Learning loop invariants for program verification,

    X. Si, H. Dai, M. Raghothaman, M. Naik, and L. Song, “Learning loop invariants for program verification,” inAdvances in Neural Information Processing Systems, vol. 31, 2018

    work page 2018

  13. [13]

    Baldur: Whole-proof generation and repair with large language models,

    E. First, M. N. Rabe, T. Ringer, and Y . Brun, “Baldur: Whole-proof generation and repair with large language models,” inProc. 31st ACM Joint European Software Engineering Conf. and Symp. Foundations of Software Engineering (ESEC/FSE), 2023

    work page 2023

  14. [14]

    SpecGen: Automated generation of formal program specifications via large language models,

    L. Ma, S. Liu, Y . Li, X. Xie, and L. Bu, “SpecGen: Automated generation of formal program specifications via large language models,” arXiv preprint arXiv:2401.08807, 2024

    work page arXiv 2024

  15. [15]

    IRIS: LLM-assisted static analysis for detecting security vulnerabilities,

    Z. Li, S. Dutta, and M. Naik, “IRIS: LLM-assisted static analysis for detecting security vulnerabilities,” inProc. Int. Conf. Learning Representations (ICLR), 2025

    work page 2025

  16. [16]

    QLCoder: A query syn- thesizer for static analysis of security vulnerabilities,

    C. Wang, Z. Li, S. Dutta, and M. Naik, “QLCoder: A query syn- thesizer for static analysis of security vulnerabilities,”arXiv preprint arXiv:2511.08462, 2025

    work page arXiv 2025

  17. [17]

    Neurosymbolic programming,

    S. Chaudhuri, K. Ellis, O. Polozov, R. Singh, A. Solar-Lezama, and Y . Yue, “Neurosymbolic programming,”Foundations and Trends in Programming Languages, vol. 7, no. 3, pp. 158–243, 12 2021. [Online]. Available: https://doi.org/10.1561/2500000049

    work page doi:10.1561/2500000049 2021

  18. [18]

    Locus: Agentic pred- icate synthesis for directed fuzzing,

    J. Zhu, C. Shen, Z. Li, J. Yu, Y . Chen, and K. Pei, “Locus: Agentic pred- icate synthesis for directed fuzzing,”arXiv preprint arXiv:2508.21302, 2025

    work page internal anchor Pith review arXiv 2025

  19. [19]

    Scallop: A language for neurosymbolic programming,

    Z. Li, J. Huang, and M. Naik, “Scallop: A language for neurosymbolic programming,”Proc. ACM Program. Lang., vol. 7, no. PLDI, pp. 1463– 1487, 2023

    work page 2023

  20. [20]

    Lobster: A gpu-accelerated framework for neurosymbolic programming,

    P. Biberstein, Z. Li, J. Devietti, and M. Naik, “Lobster: A gpu-accelerated framework for neurosymbolic programming,” in Proceedings of the 31st ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 1. ACM, Dec. 2025, p. 147–162. [Online]. Available: http://dx.doi.org/10.1145/3760250.3762232

    work page doi:10.1145/3760250.3762232 2025

  21. [21]

    Relational programming with foundational models,

    Z. Li, J. Huang, J. Liu, F. Zhu, E. Zhao, W. Dodds, N. Velingker, R. Alur, and M. Naik, “Relational programming with foundational models,”Proceedings of the AAAI Conference on Artificial Intelligence, vol. 38, no. 9, p. 10635–10644, Mar. 2024. [Online]. Available: http://dx.doi.org/10.1609/aaai.v38i9.28934

    work page doi:10.1609/aaai.v38i9.28934 2024

  22. [22]

    Retrieval-augmented generation for knowledge-intensive NLP tasks,

    P. Lewis, E. Perez, A. Piktus, F. Petroni, V . Karpukhin, N. Goyal, H. K ¨uttler, M. Lewis, W. Yih, T. Rockt ¨aschel, S. Riedel, and D. Kiela, “Retrieval-augmented generation for knowledge-intensive NLP tasks,” Advances in Neural Information Processing Systems, vol. 33, pp. 9459– 9474, 2020

    work page 2020

  23. [23]

    When LLMs meet API documentation: Can retrieval augmentation aid code generation just as it helps developers?

    J. Chen, S. Chen, J. Cao, J. Shen, and S.-C. Cheung, “When LLMs meet API documentation: Can retrieval augmentation aid code generation just as it helps developers?”arXiv preprint arXiv:2503.15231, 2025

    work page arXiv 2025