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

作者提出 DAISY，一个面向 Dafny 的故障引导断言推断工具：它借助验证器诊断、基于 LLM 的定位或两者结合来定位可能的断言位置，再用 LLM 生成候选断言并由 Dafny 验证器筛选。作者将 DafnyBench 扩展出缺失断言的失败变体，DAISY 在缺失一个断言的程序上验证通过率 86%，缺失两个断言时为 36%，且成功修复的断言常与原断言不同。