DAISY：用验证器诊断与LLM推断Dafny断言

1. 13:00
   arXiv cs.AI

   DAISY：面向 Dafny 的故障引导断言推断工具

   DAISY 是一款面向 Dafny 的故障引导断言推断工具，利用验证器诊断或 LLM 定位可能的断言位置，再由 LLM 生成候选断言并用 Dafny 验证器筛选。团队扩展 DafnyBench 构建了缺失断言变体基准，DAISY 在缺失单个断言的程序上验证通过率达 86%，缺失两个断言时为 36%。结果表明该方法能修复大量 Dafny 验证失败，且成功修复的断言常与原断言不同。

趋势仅比较持续完整观测到的相同主体，范围可能小于当前热度统计。移动指针或点击图表查看每小时热度；键盘可用左右方向键切换。