arXiv cs.AI· \'Alvaro Silva, Alexandra Mendes, Ruben Martins·· 1 天前AI 评分23
DAISY：面向 Dafny 的故障引导断言推断工具
DAISY: Fault-Guided Assertion Inference for Dafny
AI 导读
DAISY 是一款面向 Dafny 的故障引导断言推断工具，利用验证器诊断或 LLM 定位可能的断言位置，再由 LLM 生成候选断言并用 Dafny 验证器筛选。团队扩展 DafnyBench 构建了缺失断言变体基准，DAISY 在缺失单个断言的程序上验证通过率达 86%，缺失两个断言时为 36%。结果表明该方法能修复大量 Dafny 验证失败，且成功修复的断言常与原断言不同。
正文 · 原文
Abstract:Formal verification with Dafny provides strong correctness guarantees, but verification failures often require users to determine where helper assertions are needed and to manually write the assertions necessary for verification to succeed. This proof-engineering burden is difficult, time-consuming, and a barrier to the adoption of verification-aware languages.
We present DAISY (Dafny Assertion Inference SYstem), a tool for fault-guided assertion inference in Dafny.
Given a Dafny program and a target method, DAISY localizes likely assertion sites using verifier diagnostics, LLM-based localization, or their combination. It then annotates the program with assertion placeholders, retrieves relevant in-context examples, generates candidate assertions with an LLM, and validates candidates by running the Dafny verifier.
To evaluate DAISY, we extend DafnyBench with verification-failing variants created by removing helper assertions from verified programs. The resulting benchmark distinguishes between programs with one missing assertion, two missing assertions, and all assertions removed, allowing us to evaluate DAISY on increasingly difficult proof failures. On this benchmark, DAISY verifies 86\% of programs with a single missing assertion and 36\% of programs with two missing assertions. These results show that fault-guided LLM assertion inference can repair many Dafny verification failures. They also show that successful repairs often differ from the original assertions, reducing proof-engineering effort without reconstructing the original proof.
| Subjects: | Software Engineering (cs.SE); Artificial Intelligence (cs.AI); Logic in Computer Science (cs.LO); Programming Languages (cs.PL) |
| Cite as: | arXiv:2511.00125 [cs.SE] |
| (or arXiv:2511.00125v2 [cs.SE] for this version) | |
| https://doi.org/10.48550/arXiv.2511.00125 arXiv-issued DOI via DataCite |
Submission history
From: Alvaro Festas Silva [view email]
[v1]
Fri, 31 Oct 2025 09:45:39 UTC (168 KB)
[v2]
Wed, 11 Nov 2026 13:30:45 UTC (107 KB)
来源：arXiv cs.AI · arxiv.org