利用大语言模型增强复杂程序自动循环不变量生成

自动化程序验证始终是构建可信赖软件的重要组成部分。虽然对真实程序的分析仍是理论挑战，但循环不变量分析的自动化已有效解决了这一问题。然而，常混合复杂数据结构和控制流的真实程序对传统循环不变量生成工具构成挑战。为增强不变量生成技术的适用性，我们提出了ACInv——一种自动化复杂程序循环不变量生成工具，将静态分析与大语言模型（LLM）相结合，以生成每个循环的适当不变量。我们利用静态分析从每个循环中提取必要信息，并嵌入提示词中供LLM生成不变量。随后，我们采用基于LLM的评估器来评估生成的不变量，通过强化、削弱或拒绝其正确性来优化它们，从而获得增强后的不变量。我们对ACInv进行了实验，结果显示ACInv在数据结构数据集上优于以前的工具，在没有数据结构的数值程序数据集上保持与最先进工具AutoSpec的相似性能。对于总数据集，ACInv比AutoSpec可以解决21%更多的示例，并且可以生成参考数据结构模板。