SpecSyn：基于 LLM 的实际程序验证形式规范的综合和细化

程序验证是严格保证软件系统的正确性和无故障的形式化技术。然而，为完整的验证义务构建全面的过程间规范既耗时又费力，这就催生了自动化规范生成方法。尽管 大语言模型 (LLM) 在这些方法中带来了显着的进步，但现有的 LLM 授权的方法仍然受到很大的限制：它们缺乏处理大型输入程序的有效策略，并且通常没有配备评估和保证生成规范的强度的机制。这些限制削弱了它们从现实世界的复杂程序中提取精确规范以支持目标属性验证的能力，从而阻碍了现有方法在现实世界程序验证任务中的适用性。为了弥补这一差距，我们提出了 SpecSyn，一种新颖的基于 LLM 的规范生成方法。 SpecSyn 首先将输入程序分解为单独的段，这些段由后续的迭代规范生成过程分别处理。创新地，我们将基于语义非等价程序突变和变体辨别的规范细化机制纳入该过程，评估和增强生成规范的语义强度。大量实验表明，SpecSyn 保持了超过 90% 的高精度和超过 75% 的出色召回率，显着优于现有的基于 LLM 的方法。在进一步的评估中，SpecSyn 成功处理了开源程序 1365 个目标属性中的 1071 个，证明了其在实际程序验证任务中的适用性。