Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification

正式验证提供了一种严谨和系统的方法，以确保软件系统的正确性和可靠性。然而，构建完整证明的规范依赖于领域专业知识和不可忽略的人力。鉴于这种需求，需要一种自动化的规范综合方法。虽然现有的自动化方法在其通用性方面受到限制，即它们要么仅专注于为数值程序合成循环不变式，要么专门针对特定类型的程序或不变式进行调整。涉及多个复杂数据类型（例如数组、指针）和代码结构（例如嵌套循环、函数调用）的程序通常超出了它们的能力范围。为了帮助弥合这一差距，我们提出了AutoSpec，一种用于自动化程序验证规范综合的自动化方法。它克服了现有工作在规范通用性方面的缺点，为完整的证明合成了可满足和充分的规范。它由静态分析和程序验证驱动，并由大型语言模型（LLM）赋能。AutoSpec通过三种方式解决实际挑战：（1）通过静态分析和程序验证驱动，LLMs作为生成器生成候选规范，（2）将程序分解以引导LLMs的注意力，（3）在每一轮中验证候选规范，以避免在与LLMs交互过程中出现错误积累。通过这种方式，AutoSpec可以逐步和迭代地生成可满足和充分的规范。评估显示其有效性和实用性，因为它通过自动规范综合成功验证了79％的程序，这是1.592倍的显着改进。它还可以成功地应用于验证实际X509解析器项目中的程序。

AutoSpec: Automated Specification Synthesis for Automated Program Verification

AutoSpec is an automated approach to synthesize specifications for automated program verification, overcoming the limitations of existing approaches in terms of versatility. It is driven by static analysis and program verification, and is empowered by large language models (LLMs). It can incrementally and iteratively generate satisfiable and adequate specifications through the interaction with LLMs.

AutoSpec successfully verifies 79% of programs through automatic specification synthesis, a significant improvement of 1.592x compared to existing works. It can also be successfully applied to verify the programs in a real-world X509-parser project.

Related works include automated approaches for synthesizing loop invariants for numerical programs or specific types of programs or invariants. Some examples are 'Program Verification as Type Checking' and 'Loop Invariant Synthesis for Programs with Arrays and Pointers'.