PaperlayerView exact revision on arXiv

Source-linked AI summary

Integrating Symbolic Execution with LLMs for Automated Generation of Program Specifications

Fanpeng Yang, Xu Ma, Shuling Wang, Xiong Xu, Qinxiang Cao, Naijun Zhan, Xiaofeng Li, Bin Gu

arXiv:2506.09550v4cs.SE

TL;DR

Generating formal specifications for legacy programs is challenging because their control flow and data structures can be complex. SESpec combines symbolic execution, LLMs, and formal verification to generate function contracts and loop invariants, and reports stronger performance than existing methods across diverse benchmarks, including when verification goals are masked.

  • Problem

    Complex control flow and data structures make generating specifications that characterize program behavior challenging, while goal-directed specifications may not describe overall functional correctness when goals are absent.

    Source: §1 · pp. 2–3

  • Method

    SESpec combines symbolic execution and formal verification with LLM-generated loop invariants guided by symbolic results and templates, and derives specifications for loop-free code from symbolic execution.

    Source: §1 · p. 3

  • Results

    SESpec significantly outperforms existing methods across invariant and functional specification benchmarks, supports complex data structures, and maintains competitive accuracy without explicit verification goals.

    Source: §1 · p. 3, §9 · p. 25

  • Takeaways & Limitations

    The framework generates C specifications for programs involving structs, pointers, recursive types, and inductive operations, including when explicit verification goals are absent.

    Source: §1 · p. 3, §9 · p. 25

    Direct comparison with SpecGen was infeasible because it targets Java/JML rather than C/ACSL and was evaluated on a different dataset.

    Source: §7 · p. 23

Abstract

from arXiv · show

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.

1 Introduction

SESpec targets strong functional-correctness specifications, not only contracts tailored to a verification goal. It combines symbolic execution, template-guided LLM invariant generation, and formal verification to handle complex programs and reports strong results across diverse benchmarks.

1 Introduction

  • Legacy code often lacks specifications, while complex control flow and data structures make generating functionally complete contracts difficult.Goal-directed specifications may fail to describe behavior outside the target property, particularly when no explicit verification goal is available.Source: §1 · pp. 2–3

2.1 Our Approach

  • For loop-free code, symbolic execution tracks path conditions and state transitions; for loops, equality-constraint templates and those execution results guide LLM invariant generation and refinement.Verifier feedback assesses validity and accuracy, while the templates constrain the LLM’s output and reduce hallucinations and syntax errors.Source: §1 · p. 3, §2.1 · pp. 6–7
  • A flattened memory model tracks separation and aliasing, while call stacks support bottom-up, compositional handling of function calls and nested loops.Callee specifications are reused at call sites as functional summaries.Source: §1 · p. 3, §2.1 · pp. 6–7

1 Introduction

  • SESpec significantly outperforms existing methods across invariant and functional specification benchmarks, including complex data structures and masked verification goals.On numerical benchmarks it is competitive with specialized tools; under masked goals it retains high-quality specifications with a small performance drop and outperforms AutoSpec under identical masking.Source: §1 · p. 3

2 A Motivating Example And Our Approach

  • In the motivating example, LLM-generated loop invariants fail to account for loop-entry conditions and may use array abstractions unsupported by the verifier.The example also requires specifications to handle pointer aliasing, memory safety, writes, and unchanged struct fields.Source: §2 · pp. 4, 6

3 Pre-/Postcondition Specification Generation

For loop-free code, SESpec uses symbolic execution to characterize reachable states and derive strongest specifications. Its function-generation procedure pauses at loops and calls to generate invariants or callee specifications, then resumes execution to produce function contracts.

3.1 Symbolic Execution and Strongest Pre-/Postconditions

  • Symbolic execution tracks path conditions and symbolic stores across branches, representing reachable program states as sets of path-specific symbolic states.The flattened memory model represents accessible atomic memory locations as symbolic variables and explicitly tracks memory values and aliasing.Source: §3.1 · p. 8
  • A strongest postcondition is the disjunction of all symbolic states reachable at an endpoint from the starting point under a precondition.For loop-free straightline code, the weakest precondition and strongest postcondition together describe input/output behavior.Source: §3.1 · p. 8

3.2 Generation of Program Specifications

  • FuncSpec initializes a default precondition, symbolically executes until a loop, call, or function exit, and derives postconditions from the resulting states.At loops it invokes invariant generation; at calls it recursively generates a callee specification, then resumes execution using the generated annotations.Source: §3.2 · pp. 9–10

4 Loop Invariant Generation

The section frames loop-invariant generation as finding formulas that preserve program behavior and, when a postcondition exists, imply it. SESpec combines symbolic execution, LLM-generated invariants, structured templates, and verifier feedback to produce strong invariants, including when no postcondition is supplied.

4 Loop Invariant Generation

  • Loop invariants must be preserved through an iteration and, when a postcondition is supplied, imply it at termination; SESpec also targets strong invariants without postconditions.The approach uses symbolic execution and equality-based templates to capture relationships between symbolic states.Source: §4 · p. 10

4.1 Invariant Generation for Loops

  • Outer-loop generation combines program comprehension, symbolic loop analysis, template construction, LLM synthesis, and verifier-guided refinement.The LLM first analyzes the loop in natural language; templates then guide synthesis, and refinement repairs or strengthens invariants until verified.Source: §4.1 · p. 11

4.2 Loop Analysis

  • Nested loops are processed bottom-up using LLM inference without preconditions or templates, because their preconditions are not well-defined.For the outermost loop, symbolic execution of a single-iteration unfolding supports invariant generation and identifies unchanged and non-inductive variables.Source: §4.2 · p. 11

4.3 Template Generation

  • Templates encode variable behavior using symbolic execution results, while leaving undetermined parameters for the LLM to complete.They constrain output toward ACSL syntax and strong invariants covering relevant variable behavior across execution paths.Source: §4.3 · p. 12

4.4 Loop Invariant Refinement

  • Because generated invariants may be invalid or too weak, iterative refinement uses verifier feedback to repair, adjust, strengthen, weaken, or regenerate them.Repeatedly invalid invariants are eliminated; refinement stops when an invariant is verified or the iteration limit is reached.Source: §4.4 · pp. 12–13

5 Implementation

The implementation connects symbolic execution, LLM specification generation, and formal verification through a translation layer. Prompting guides generation and refinement, with examples calibrating the LLM for inductive specifications.

5.1 Toolchain Integration and Data Flow

  • The toolchain sends C code through symbolic execution, translates symbolic states for the generator and verifier, and feeds verified specifications back for further execution.Failed verification returns translated error context to the generator for iterative refinement.Source: §5.1 · pp. 13–14
  • QCP supplies symbolic execution results and Frama-C discharges proof obligations, combining intermediate-state access with automated verification.QCP supports complex data structures but requires annotations; the generator synthesizes candidate invariants, while Frama-C provides an ACSL interface and SMT-backed verification.Source: §5.1 · p. 14

5.2 Prompt Designs

  • Prompting structures loop-invariant generation and selects refinement instructions based on verifier-identified deficiencies.Textbook examples over arrays and singly linked lists calibrate the LLM to inductive-predicate syntax and semantics, supporting linked-list and arithmetic-inductive programs without training or large-scale external data.Source: §5.2 · p. 16

6 Experiments

The experiments evaluate SESpec on established and newly constructed program benchmarks using specified verification and language-model configurations. The supplied passages describe the evaluation setup, not its outcomes.

6.1 Experimental Setup

  • The benchmark suite combines established datasets with pIp, list-S, and numer-S, added to cover aerospace pointer and struct code, singly linked lists, and more difficult numerical loops.pIp comes from an aerospace control system; numer-S includes 20 linear and 20 nonlinear loops.Source: §6.1 · p. 17
  • Verification uses Frama-C 29.0 with WP, a 3-second query timeout, Z3, and the Typed memory model.Source: §6.1 · p. 17
  • The evaluation tests GPT-3.5-turbo, GPT-4o-mini, GPT-4o, and Claude-3.7-sonnet at a fixed sampling temperature of 0.7.Source: §6.1 · p. 17

• RQ4: What are the Advantages of SESpec Over Other Work?

SESpec is evaluated across program types, specification-generation settings, and comparisons with existing tools. The results show broad applicability, gains from symbolic execution and refinement, and performance across numerical and data-structure benchmarks, including settings without verification goals.

6.2 RQ1: What Types of Programs can SESpec Manage?

  • SESpec successfully verifies 354 of 395 programs, but its success rate falls from 97% on linear-loop and iteration-free programs to 63% on nested and multi-loop programs.The evaluation includes loop-only and full-specification programs; the paper identifies complex invariant synthesis, rather than lines of code, as the main difficulty.Source: §6.2 · pp. 17–18, Table 1 · p. 17

6.3 RQ2: How does SESpec Perform on Program Specification Generation?

  • Across models, SESpec narrows performance gaps at higher Pass@k levels, while gaps among syntax, validity, and accuracy become more pronounced for harder benchmarks and weaker models.The authors note that validity does not simply coincide with syntactic correctness, consistent with specifications needing to capture program semantics.Source: §6.3 · p. 18, Table 2 · p. 19

Frama-C

  • On the Frama-C benchmark, complex loops involving arrays, external calls, and recursive behaviors remain challenging for symbolic execution despite improvements from Pass@1 to Pass@5.For OOPSLA and SV-COMP, the paper also cites nested or multiple loops and difficulty deriving sufficiently strong preconditions.Source: §6.3 · p. 18, Frama-C · pp. 19–20

6.4 RQ3: Is SESpec Effective?

  • Symbolic execution raises validity and accuracy by an average of 30%, while refinement achieves perfect scores in one setting and improves validity and accuracy by 20% on average in the other.The ablation used 100 randomly chosen programs and capped refinement at three iterations.Source: §6.4 · p. 20, Figure 5 · p. 20

6.5 RQ4: What are the Advantages of SESpec Over Other Work?

  • SESpec outperforms ACInv across four AutoSpec datasets, and GPT-4o yields steady gains for SESpec while AutoSpec shows negligible improvement over GPT-3.5-turbo.The comparison covers three LLM-based approaches; the supplied table caption identifies Table 3 as the performance comparison.Source: §6.5 · p. 21, Table 3 · p. 21
  • On SyGuS, SESpec reaches 100% success and on OOPSLA 87%; it matches LiPus on NLA but trails CLAUSE2INV there by 10%.The paper notes that the SMT-based comparison tools are specialized for numerical loops.Source: §6.5 · p. 22
  • On pIp, SESpec achieves an average 50% higher success rate than AutoSpec; it also supports Frama-C and linked-list specifications through inductive predicates.The pIp benchmark contains extensive structure and pointer operations; the paper attributes its result to flattened memory modeling and precise symbolic execution.Source: §6.5 · p. 22
  • Without verification goals, SESpec accuracy falls from 93.98% to 80.45% on syGus and from 70.83% to 64.71% on Frama-C, while AutoSpec drops more sharply.The authors attribute SESpec’s drop primarily to goal-targeted refinement; without that refinement gain, its performance across the settings is nearly identical.Source: Figure 6 · p. 20, §6.5 · pp. 22–23

7 Threats to Validity

The section addresses evaluation bias and leakage by avoiding external supervision and dataset dependencies, while using established benchmarks plus a harder original set to assess performance and comparability.

Data Leakage

  • The approach avoids fine-tuning, retrieval, synthesized datasets, and few-shot prompting, grounding LLM reasoning in symbolic states from the target program to mitigate benchmark leakage and overfitting.The authors say this design strengthens internal validity by minimizing bias and preventing data leakage.Source: §7 · p. 23

Benchmark and Baseline Selection

  • The evaluation uses the AutoSpec benchmark and external Lipus and Clause2Inv datasets, plus pIp, which has more complex data structures and control flow.The selected established sets are described as comparable in loop complexity and lines of code.Source: §7 · p. 23
  • SpecGen [22] is excluded because its Java/JML setting differs from the paper’s C/ACSL setting and it was evaluated on a custom dataset rather than the AutoSpec benchmark.The authors frame the selected benchmarks as supporting comparison with prior work and evaluation on complex software.Source: §7 · p. 23

8 Related Work

Related work spans dynamic and static inference, machine-learning and SMT-based methods, and LLM-based specification tools. The paper reports competitive performance against invariant-generation methods on numeric benchmarks and compares its approach with C-oriented tools.

Traditional approach

  • Dynamic methods infer candidates from execution traces, but their effectiveness depends on test-suite coverage and quality.Daikon uses predefined templates, while DIG infers from traces using equation solving, polyhedra construction, and theorem proving.Source: §8 · p. 24
  • Static methods include constraint solving, abstract interpretation, interpolation, recurrence analysis, and shape analysis, but are often specialized, unscalable, or dependent on manual intervention.The cited limitations include double-exponential constraint solving, abstraction precision loss, and recurrence methods restricted to cases with suitable closed forms or conditions [13].Source: §8 · p. 24

Machine learning and SMT-based approach

  • Machine-learning and SMT-based tools such as CODE2INV, LIPuS, and Clause2Inv address invariant synthesis but are largely numeric, produce SMT-format invariants, and rely on supplied verification goals.The passage also describes Clause2Inv as an LLM candidate-generation and counterexample-driven combination approach.Source: §8 · p. 24
  • On numeric benchmarks, the paper reports competitive performance and, in some cases, better results than the compared methods.The paper identifies ACInv [21] and AutoSpec [32] as detailed C-program comparisons.Source: §8 · p. 25

LLM-based approach

  • LLM-based tools use different guidance and verification strategies, including mutation-based recovery in SpecGen [22], static-analysis context in ACInv [21], and decomposition with few-shot prompts in AutoSpec [32].The passage describes AutoSpec as verifying generated specifications with Frama-C.Source: §8 · p. 25

9 Conclusion

The paper concludes that its end-to-end framework generates C specifications and reports gains across benchmarks, including support for complex data structures. It identifies more complex recursion and nested-loop invariants as future work.

9 Conclusion

  • The framework integrates symbolic execution, LLMs, and formal verification to generate C loop invariants and preconditions and postconditions.The authors report that it significantly outperforms existing methods across diverse benchmarks in invariant and functional specification generation.Source: §9 · p. 25
  • Flattened memory modeling and inductive predicates support structs, pointers, recursively defined types such as singly linked lists, and inductive operations.The conclusion also reports competitive accuracy without explicit verification goals and says the method consistently surpasses prior tools.Source: §9 · p. 25
  • Future work targets more complex recursive structures and functions, and stronger invariant generation for nested loops with correlated induction variables.The authors propose symbolic sampling and targeted training strategies to improve nested-loop invariant precision.Source: §9 · p. 25
Loading 2506.09550v4…