paperbot · PL 论文追踪

全部论文 待读 收藏

P1 DafnyRAG: A Retrieval-Augmented and Verification-Driven Tool for Automated Repair of Dafny Code

DafnyRAG：一个检索增强与验证驱动的 Dafny 代码自动修复工具
ASE Proceedings of the 41st IEEE/ACM International Conference on Automated Software Engineering2026匹配度 7/10 · 该论文将检索增强生成与形式验证反馈结合用于修复 Dafny 代码和提升规约准确性，直接落在“LLM/Agent 改进形式化验证”这一兴趣方向。但它更偏自动修复而非静态分析或 Agentic 程序分析，也未涉及浮点或贝叶斯程序分析。引用 1 inbox
Yanzhen Liu, Xu Lu, Bin Yu, Haoxiang Zhang, Chu Chen, Meng Wang
测试、调试与修复机器学习与程序语言
crossref: 2026-10-09

AI 速览

一句话：提出结合形式验证反馈与检索增强生成来迭代修复 Dafny 代码并提升形式规约准确性的工具。

在 Dafny 等支持形式验证的语言中，程序正确性依赖精确的形式规约，而规约中常存在不完整或错误，导致验证失败。人工修复这些规约与代码需要理解验证器反馈并具备领域知识，成本高昂。DafnyRAG 将形式验证反馈作为修复信号，在迭代循环中结合检索增强生成：先从已有 Dafny 代码库中检索相似规约与证明片段，再由生成模型产生候选修复，并依据验证结果决定是否继续迭代。该工具的目标是自动修复 Dafny 代码，提高形式规约的准确性，最终使程序通过验证。摘要未报告具体实验数据与基准结果。

问题
Dafny 代码的形式规约常不准确，导致验证失败，而人工根据验证反馈修复规约与代码既困难又耗时。
方法
DafnyRAG 以形式验证反馈驱动迭代修复，并引入检索增强生成，从已有 Dafny 代码中检索相关规约或证明片段来指导修复。
评估
摘要未给出具体实验设置与量化结果；该工作以验证反馈和迭代修复提升规约准确性为目标，评估应关注 Dafny 程序的验证通过情况。
原文摘要（Abstract）

A system that iteratively repairs Dafny code by leveraging formal verification feedback and retrieval-augmented generation to improve formal specification accuracy.

链接与引用

DOI 原文 · PDF（开放获取） ·

BibTeX 
@inproceedings{paperbot12412,
  title = {DafnyRAG: A Retrieval-Augmented and Verification-Driven Tool for Automated Repair of Dafny Code},
  author = {Yanzhen Liu and Xu Lu and Bin Yu and Haoxiang Zhang and Chu Chen and Meng Wang},
  booktitle = {ASE},
  year = {2026},
  doi = {10.1145/3832783.3834610}
}