Pith. sign in

REVIEW 5 cited by

Lemur: Integrating Large Language Models in Automated Program Verification

Not yet reviewed by Pith; the record is open.

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

This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.

SPECIMEN: schema-true, not a live event

T0 review · schema-true

One-sentence machine reading of the paper's core claim.

pith:XXXXXXXX · record.json · timestamp

arxiv 2310.04870 v5 pith:5SYYQOBL submitted 2023-10-07 cs.FL cs.AIcs.LGcs.LO

Haoze Wu , Clark Barrett , Nina Narodytska This is my paper · ORCID
classification cs.FLcs.AIcs.LGcs.LO
keywords automatedverificationprogramllmsmethodologyabstractbenchmarkscalculus
verification ladder T0 review T1 audit T2 compute T3 formal
0 comments
read the original abstract

The demonstrated code-understanding capability of LLMs raises the question of whether they can be used for automated program verification, a task that demands high-level abstract reasoning about program properties that is challenging for verification tools. We propose a general methodology to combine the power of LLMs and automated reasoners for automated program verification. We formally describe this methodology as a set of transition rules and prove its soundness. We instantiate the calculus as a sound automated verification procedure and demonstrate practical improvements on a set of synthetic and competition benchmarks.

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 5 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. An AI Approach to Verified Production Cryptographic Libraries

    cs.CR 2026-08 conditional novelty 6.0 of 10

    An AI agent, guarded by mechanical integrity gates, synthesized Verus-verified internal specifications and proofs for curve25519-dalek and chacha20 without changing executable code.

  2. LimICE: Integrating LLM into ICE Framework for Efficient Loop Invariant Inference

    cs.SE 2026-07 conditional novelty 6.0 of 10

    LimICE combines LLM-generated facts, incremental lemma synthesis, and a decision-tree fallback to solve 349/367 linear and 47/50 nonlinear loop-invariant benchmarks, beating state-of-the-art tools.

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

    cs.SE 2026-07 conditional novelty 5.5 of 10

    Mid-tier reasoning LLMs with consistency checks and LLM reasoning evaluation adjudicate static-analysis alerts at ≥98% recall and ≥94.8% specificity across Juliet, FormAI, and SV-COMP.

  4. The 4/$\delta$ Bound: Designing Predictable LLM-Verifier Systems for Formal Method Guarantee

    cs.AI 2025-11 reject novelty 2.0 of 10

    The 4/δ bound is the mean of four geometric distributions, not a new theorem, and the simulation validation is circular.

  5. A Short Survey on Formalising Software Requirements using Large Language Models

    cs.SE 2025-06 unverdicted novelty 1.0 of 10

    A survey summarizing 35 papers on using LLMs to formalize software requirements, but it contains no new experimental results and its classification tables have errors.

Pith tools