Source-linked AI summary
Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification
Cheng Wen, Jialun Cao, Jie Su, Zhiwu Xu, Shengchao Qin, Mengda He, Haokun Li, Shing-Chi Cheung, Cong Tian
TL;DR
Automated specification synthesis is needed because full formal proofs require substantial domain expertise, while existing approaches are limited in the program and specification types they handle. AutoSpec combines static analysis and verification with decomposed, iterative LLM generation and validation; it successfully handles 79% of benchmark programs and is applied to an X509-parser project.
Problem
Existing automated synthesis approaches are limited in the specification types and program structures or data types they can handle, while constructing specifications for full proofs remains labor-intensive.
Source: §1 · p. 2Method
AutoSpec uses static analysis and program verification to guide LLM generation of candidate specifications, decomposing programs and validating candidates iteratively.
Source: §1 · p. 3, §3.1 · p. 7, §3.3 · p. 11Results
79% (199/251) of programs across four benchmarks were successfully handled by AutoSpec, 59.2% more than existing approaches; it also generated specifications for six X509-parser functions within minutes.
Source: §1 · pp. 3–4Takeaways & Limitations
AutoSpec synthesized satisfiable and adequate specifications for programs with varied structures in the evaluated benchmarks and for six functions in a real-world X509-parser project.
Source: §1 · p. 3Completing verification for the entire X509-parser project remains challenging, despite successful specification synthesis for six of its functions.
Source: §5 · p. 19
Abstract
from arXiv · showhide
Formal verification provides a rigorous and systematic approach to ensure the correctness and reliability of software systems. Yet, constructing specifications for the full proof relies on domain expertise and non-trivial manpower. In view of such needs, an automated approach for specification synthesis is desired. While existing automated approaches are limited in their versatility, i.e., they either focus only on synthesizing loop invariants for numerical programs, or are tailored for specific types of programs or invariants. Programs involving multiple complicated data types (e.g., arrays, pointers) and code structures (e.g., nested loops, function calls) are often beyond their capabilities. To help bridge this gap, we present AutoSpec, an automated approach to synthesize specifications for automated program verification. It overcomes the shortcomings of existing work in specification versatility, synthesizing satisfiable and adequate specifications for full proof. It is driven by static analysis and program verification, and is empowered by large language models (LLMs). AutoSpec addresses the practical challenges in three ways: (1) driving \name by static analysis and program verification, LLMs serve as generators to generate candidate specifications, (2) programs are decomposed to direct the attention of LLMs, and (3) candidate specifications are validated in each round to avoid error accumulation during the interaction with LLMs. In this way, AutoSpec can incrementally and iteratively generate satisfiable and adequate specifications. The evaluation shows its effectiveness and usefulness, as it outperforms existing works by successfully verifying 79% of programs through automatic specification synthesis, a significant improvement of 1.592x. It can also be successfully applied to verify the programs in a real-world X509-parser project.
1 Introduction
AutoSpec addresses the limited versatility of automated specification synthesis by combining LLM-generated candidates with static analysis, program verification, decomposition, and iterative validation. Across four benchmarks, it successfully handles 79% of 251 programs, including structures that existing approaches cannot handle, and is also applied to an X509-parser project.
Research gap
- Prior approaches focus on particular specification types or numerical programs, limiting their ability to handle varied code and data structures together.The paper identifies invariants, preconditions, and postconditions, as well as multiple or nested loops, arrays, and pointers, as dimensions of this versatility gap.Source: §1 · p. 2
Challenges
- LLM specification synthesis faces errors, attention limitations in long contexts, and error accumulation when incorrect outputs are reused.The paper notes that specifications are less familiar in LLM training than programming languages and that holistic synthesis may yield unsatisfactory results.Source: §1 · p. 2
Approach
- AutoSpec uses static analysis and program verification to guide LLMs in generating candidate specifications for selected program pieces.It decomposes programs hierarchically and generates specifications incrementally in a bottom-up manner.Source: §1 · pp. 2–3
Specification validation
- The approach validates candidates in each round, discarding specifications inconsistent with program behavior and retaining validated ones for subsequent synthesis.Generation continues until specifications are adequate to prove the target property or a predefined iteration limit is reached.Source: §1 · p. 3
Evaluation
- 79% (199/251) of programs were successfully handled by AutoSpec, which handled 59.2% more programs than existing approaches and was applied to six X509-parser functions.The experiments covered four benchmarks; the X509-parser functions were handled within a few minutes.Source: §1 · pp. 3–4
2 Background and Motivation
The bubble-sort example illustrates the substantial manual work involved in writing specifications for a full proof, while prior automated methods handle only limited program settings. AutoSpec proposes bottom-up synthesis of multiple specification types, validates them, and provides an automated verification workflow.
Motivation
- Writing specifications for the bubble-sort example is non-trivial, motivating automation beyond existing methods limited to loop invariants for numerical programs.The example uses ACSL annotations to prove that the sorted array is in ascending order.Source: §2 · pp. 4–5
AutoSpec
- A full proof may require preconditions, postconditions, loop invariants, and assigned-variable specifications, which AutoSpec synthesizes bottom-up.The example traces from the target property through function calls and nested loops, adding specifications along the way.Source: §2 · p. 5
Validation
- Specifications are checked for satisfiability during synthesis and for adequacy against the target property after synthesis.The intended outcome is a set of specifications that both satisfy the program and suffice to verify the desired property.Source: §2 · pp. 5–6
User scenario
- AutoSpec takes a program and properties through specification synthesis, validation, verification, and output of a proof when available.For a semantically buggy program, adequate specifications may not be synthesized before the maximum iteration count is reached.Source: §2 · p. 6
3 Methodology
AutoSpec decomposes programs into components, generates specifications bottom-up with LLMs, and validates them with a theorem prover. The workflow iterates until the target property is proved or the iteration limit is reached.
3.1 Code Decomposition
- AutoSpec builds an extended call graph from the target assertion, representing loops as nodes to identify where specifications belong and in what order to add them.The graph is constructed by traversing the source AST for functions, loops, and their calling relationships; specifications for each node need consider its code and callees.Source: §3.1 · p. 7
3.2 Hierarchical Specification Generation
- Specifications are generated from graph leaves toward the root, with placeholders filled by validated candidates over iterations until the assertion is proved or the iteration bound is reached.For each component, AutoSpec retains valid specifications and generates additional ones if the whole verification task remains incomplete.Source: §3 · p. 7, §3.2 · pp. 8–9
- Prompts provide a role, task description, examples, and a highlighted code placeholder, while omitting code irrelevant to the component being specified.Few-shot examples can teach specification-language syntax and semantics through in-context learning.Source: §3.2 · p. 10
3.3 Specification Validation
- AutoSpec checks candidate specifications for legality and satisfiability, postponing loop satisfiability checks until the outermost loop because inner loops may use outer-loop variables.Frama-C helps identify illegal or unsatisfiable candidates, which are removed while remaining candidates are checked.Source: §3.3 · pp. 10–11
- AutoSpec also checks whether the generated specifications suffice to prove the target assertion, distinguishing adequate specifications from those that are merely legal and satisfiable.If verification remains incomplete, another iteration generates additional specifications while retaining those already generated.Source: §3.2 · p. 9, §3.3 · p. 11
- After successful verification, optional simplification removes specifications one by one while the assertion remains verifiable, yielding a minimal set for manual reading.The procedure can remove weak or semantically similar specifications without affecting verification.Source: §3.3 · p. 11
4 Evaluation
The evaluation examines AutoSpec’s effectiveness on general specifications and loop invariants, efficiency, and design components across four benchmarks and a real-world project. It also includes case studies illustrating iterative enhancement and a failure linked to missing context.
4.1 Evaluation Setup
- The benchmarks cover multiple functions or loops, nested or multiple loops, and linear loops; the evaluation assumes programs compile and their properties are consistent with the code.The paper describes Frama-C-problems and X509-parser as involving multiple functions or loops, SyGuS as having linear loops, and OOPSLA-13 and SV-COMP as including nested or multiple loops.Source: Benchmark · p. 13
4 Evaluation
- The evaluation compares AutoSpec with existing approaches for loop invariants and separately tests its design through ablation.The study also measures overhead and evaluates general specification generation, including a real-world project.Source: §4 · p. 12, Benchmark · p. 12, Baselines · p. 13
4.2 RQ1. Effectiveness on General Specification
- AutoSpec successfully solved 31 of 51 programs; in the X509-parser project, it solved all six manually selected representative functions, though applying it seamlessly to the entire project remained impractical without human intervention.The whole-project specifications had been manually added over five months.Source: §4.2 · pp. 13–14
4.3 RQ2. Effectiveness on Loop Invariants
- On SyGuS, AutoSpec solved 114 programs versus CLN2INV’s 124; on OOPSLA-13, AutoSpec solved 38/46 while CLN2INV scored 0/46.On SV-COMP, AutoSpec solved 16/21 programs in an average of 3 minutes; among three programs with 3-fold nested loops, it solved one.Source: §4.3 · pp. 15–16
4.4 RQ3. Efficiency of AutoSpec
- Across four benchmarks, validation and verification took 1.3–994.9 seconds, while LLM querying averaged under 10 seconds; specification simplification was optional.AutoSpec’s validation took 1.2 seconds to 3.88 minutes, compared with cited prior approaches’ one- to 12-hour validity checks; simplification time varied with the number of generated specifications.Source: §4.4 · p. 16
4.5 RQ4. Ablation Study
- The ablation results rose from 5 to 31 solved programs out of 51, with decomposition and hierarchical specification generation producing the largest reported improvement, from 9 to 26.The reported increase from one pass to five iterations was 27 to 31 solved programs.Source: §4.5 · p. 17
4.6 Case Studies
- In the pointer-sum case, a second enhancement round supplied a specification that the add function had no assignment behavior, allowing verification to succeed.The first-round specifications were inadequate because they did not describe whether pointer values changed within add.Source: §4.6 · p. 17
- In the pow case, AutoSpec could not generate an adequate specification because its prompt lacked the unavailable function’s code and dependencies.The paper identifies including more dependencies in the prompt as a possible improvement.Source: §4.6 · p. 18
5 Threats to Validity
The authors examine data leakage, generalizability across LLMs, and scalability. Mutation tests largely preserved results, while completing verification of the entire X509-parser project remains challenging.
5 Threats to Validity
- 98% of results held after semantic-preserving mutations, further supporting the authors’ assessment that data-leakage risk is low.The test mutated 100 sampled programs from SyGuS, OOPSLA-13, and SV-COMP through variable renaming and statement or branch switching.Source: §5 · p. 18
- 25/51 programs were verified with AutoSpec (Llama2), compared with 31/51 using AutoSpec (ChatGPT) on the same RQ1 benchmark.Source: §5 · p. 19
- Completing verification of the entire X509-parser project remains challenging, although the project evaluation achieved unexpectedly good performance.The authors say the evidence suggests AutoSpec has potential to assist participants writing specifications for real-world programs.Source: §5 · p. 19
6 Related Work
Related work spans specification inference and LLM-assisted program analysis. AutoSpec differs by generating varied specifications for verification rather than whole proofs or other analysis outputs.
6 Related Work
- Prior work covers natural-language generation, data mining, static inference, loop invariants, termination, and Java class specifications.The paper says AutoSpec instead statically generates comprehensive contracts for each loop and function.Source: §6 · p. 19
- AutoSpec is presented as statically generating comprehensive contracts for loops and functions to support reliable verification outcomes.Source: §6 · p. 19
- LLM studies address fuzz testing, static analysis, verification [61] [62], bug reproduction, and repair; Baldur generates and repairs proofs, unlike AutoSpec’s specification focus.AutoSpec complements these efforts with practical program specifications [26].Source: §6 · pp. 19–20
7 Conclusion
AutoSpec generates candidate specifications bottom-up from source code, validates them with provers or verification tools, and iteratively enhances them. The evaluation reports full automation and cost-effectiveness for specification generation, addressing a formal-verification bottleneck.
7 Conclusion
- AutoSpec generates candidate specifications from source code bottom-up, validates them with provers or verification tools, and iteratively enhances them.The authors report that evaluation demonstrates full automation and cost-effectiveness in specification generation, a major formal-verification bottleneck.Source: §7 · p. 20