软件工程领域顶级会议ICSE'26近日公布论文录用名单，程序设计语言研究室两篇论文被该会议录用。

论文1

标题： PredicateFix: Repairing Static Analysis Alerts with Bridging Predicates.

作者： Yuan-an Xiao, Weixuan Wang, Dong Liu, Junwei Zhou, Shengyu Cheng, Yingfei Xiong.

摘要： 使用大型语言模型（LLMs）修复静态分析警报（static analysis alerts）在程序代码中正变得日益流行和有帮助。然而，这些模型经常存在幻觉问题，并且在处理复杂和罕见的警报时表现不佳，从而限制了其性能。为了应对这一挑战，本文利用分析规则中的谓词（predicates），这些谓词可以作为警报与干净代码库中相关代码片段（称为“关键示例”）之间的桥梁。基于这一洞察，我们提出了一种算法，能自动检索警报的关键示例。然后，我们构建了PredicateFix作为一个RAG（检索增强生成）流程，用于修复由CodeQL代码检查器和另一款用于Golang的命令式静态分析器标记的警报。使用多个LLM进行的评估表明，PredicateFix将正确修复的数量增加了27.1%至72.5%，显著优于其他基准RAG方法。

论文2

标题： HoarePrompt: Structural Reasoning About Program Correctness in Natural Language.

作者： Dimitrios Stamatios Bouras, Yihan Dai, Tairan Wang, Yingfei Xiong, Sergey Mechtaev.

摘要： 尽管软件需求通常用自然语言表达，但根据自然语言需求来验证程序的正确性是一个困难且未被充分探索的问题。为了解决这一差距，我们引入了HoarePrompt，这是一种新颖的方法，它将程序分析和验证的基本思想应用于自然语言产物。从最强后置条件演算（strongest postcondition calculus）中汲取灵！，HoarePrompt采用一种系统的、逐步的过程，其中LLM在代码的各个点生成对可达程序状态的自然语言描述。为了管理循环，我们提出了“少样本驱动的k-归纳法”（few-shot-driven k-induction），这是对模型检查中广泛使用的k-归纳法的一种改编。一旦程序状态被描述，HoarePrompt便利用LLM来评估带有这些状态描述的程序是否符合自然语言需求。我们的实验表明，与直接使用Zero-shot-CoT提示进行正确性分类相比，HoarePrompt将MCC（马修斯相关系数）提高了62%。此外，HoarePrompt通过将MCC提高93%，其表现优于一个通过基于LLM的测试生成来评估正确性的分类器。