Automatically generating formal specifications including loop invariants, preconditions, and postconditions for legacy code is critical for program understanding, reuse and verification. However, the inherent complexity of control and data structures in programs makes this task particularly challenging. This paper presents a novel framework that integrates symbolic execution with large language models (LLMs) to automatically synthesize formally verified program specifications. Our method first employs symbolic execution to derive precise strongest postconditions for loop-free code segments. These symbolic execution results, along with automatically generated invariant templates, then guide the LLM to propose and iteratively refine loop invariants until a correct specification is obtained. The template-guided generation process robustly combines symbolic inference with LLM reasoning, significantly reducing hallucinations and syntactic errors by structurally constraining the LLM's output space. Furthermore, our approach can produce strong specifications without relying on externally provided verification goals, enabled by the rich semantic context supplied by symbolic execution, overcoming a key limitation of prior goal-dependent tools. Extensive evaluation shows that our tool SESpec outperforms the existing state-of-the-art tools across numerical and data-structure benchmarks, demonstrating both high precision and broad applicability.

翻译：为遗留代码自动生成包含循环不变式、前置条件与后置条件的形式化规约，对于程序理解、重用与验证至关重要。然而，程序控制流与数据结构的固有复杂性使得该任务极具挑战性。本文提出一种创新框架，通过集成符号执行与大语言模型（LLMs）来自动合成经形式化验证的程序规约。我们的方法首先运用符号执行为无循环代码段推导精确的最强后置条件；这些符号执行结果与自动生成的不变式模板共同引导LLM提出并迭代优化循环不变式，直至获得正确的规约。该模板引导的生成过程将符号推理与LLM推理鲁棒地结合，通过对LLM输出空间进行结构化约束，显著减少了幻觉与语法错误。此外，得益于符号执行提供的丰富语义上下文，我们的方法无需依赖外部给定的验证目标即可生成强规约，从而克服了先前依赖目标的工具的关键局限。大量实验表明，我们的工具SESpec在数值与数据结构基准测试中均优于现有最先进工具，展现出高精度与广泛适用性。