Integrating Symbolic Execution with LLMs for Automated Generation of Program Specifications

TL;DR

This paper introduces a novel framework combining symbolic execution and large language models to automatically generate accurate, verified program specifications, including invariants and pre/postconditions, improving over existing methods.

Contribution

The paper presents a new template-guided approach that integrates symbolic execution with LLMs to synthesize and refine program specifications without external verification goals.

Findings

Outperforms state-of-the-art tools on benchmarks

Achieves high precision in specification synthesis

Effectively handles numerical and data-structure programs

Abstract

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.