SpecSyn: LLM-based Synthesis and Refinement of Formal Specifications for Real-world Program Verification Lezhi Ma1 , Shangqing Liu1 , Yi Li2 , Qiong Wu1 , Han Wang1 , and Lei Bu1 Nanjing University, Jiangsu Province, China, [email protected], [email protected], [email protected], [email protected], [email protected] 2 Nanyang Technological University, Singapore, [email protected].
arXiv:2604.21570v1 [cs.SE] 23 Apr 2026
1
Abstract. Program verification is a formal technique to rigorously ensure the correctness and fault-freeness of software systems. However, constructing comprehensive interprocedural specifications for full verification obligations is time-consuming and labor-intensive, giving rise to automated specification generation approaches. Despite the significant advancements in these approaches brought by Large Language Models (LLMs), existing LLM-empowered approaches still suffer from significant limitations: they lack effective strategies for handling sizable input programs, and are typically equipped with no mechanisms to evaluate and guarantee the strength of the generated specifications. The limitations impair their ability to extract precise specifications from real-world complicated programs to support the verification of target properties, thereby hindering the applicability of existing approaches in verification tasks on real-world programs. To remedy this gap, we propose SpecSyn, a novel LLM-based specification generation method. SpecSyn first decomposes the input program into individual segments, which are handled respectively by the subsequent iterative specification generation process. Innovatively, we incorporate into the process a specification refinement mechanism based on semantic-non-equivalent program mutations and variant discrimination, assessing and enhancing the semantic strength of the generated specifications. Extensive experiments show that SpecSyn maintains high precision over 90% and outstanding recall over 75%, significantly outperforming existing LLM-based approaches. In further evaluations, SpecSyn successfully handles 1071 out of 1365 target properties for open-source programs, proving its applicability on real-world program verification tasks. Keywords: Program Specification · Program Verification · Large Language Models
1
Introduction
Program verification is a technique to rigorously ensure the compliance of a given program with certain properties [30], by formalizing the properties into formal
2
Lezhi Ma, Shangqing Liu, Yi Li, Qiong Wu, Han Wang, and Lei Bu
program specifications [47, 17] and proving their correctness with static analysis approaches such as theorem proving [27, 15]. Due to the wide existence of complex control-flow structures (e.g., function calls and loops) within real-world programs, the verification of high-level target properties necessitates interprocedural supporting specifications as a foundation [75]. On account of the intricate and rigorous nature of formal specifications, manually crafting specifications inevitably poses an enormous burden on developers and experts, giving rise to the research on automated specification generation techniques. In recent years, the emergence and widespread adoption of Large Language Models (LLMs) [59, 14, 60, 38, 37] have injected new momentum into automated specification generation approaches [21, 53, 75, 76], significantly enhancing both the diversity and expressiveness of generated specifications compared to traditional approaches. Nevertheless, existing LLM-empowered approaches still suffer from limitations in different aspects. On the one hand, approaches such as AutoSpec [76] and SpecGen [53] treat the input programs holistically and load the entire input program into the context of LLMs for generation. The practice typically triggers the attention dispersion problem [56] in LLMs and impairs LLM performance as input program length increases, introducing serious scalability issues and thereby hindering their usability on verification tasks of real-world complex programs. Despite the function-level decomposition technique proposed by a concurrent approach, Preguss [75], the mechanism is rather primitive and cannot handle circular dependencies between program structures. On the other hand, recent approaches tend to focus primarily on specification correctness, while mechanisms for evaluating and refining the semantic strength of specifications remain largely underexplored. Consequently, the strength of the generated specifications cannot be effectively guaranteed, making them insufficient to support the verification of target properties and ultimately limiting the applicability of existing approaches to real-world program verification tasks. These limitations present a fundamental challenge in specification generation: How to generate precise and useful specifications from sizable, complex real-world programs, so as to effectively support the verification of target properties? Confronted with the proposed challenge, we present SpecSyn, a novel LLMbased framework for formal program specification generation. Overall, the framework adopts a divide-and-conquer design to enhance its scalability: it first performs static dependency analysis to decompose the input program into a sequence of program segments together with their dependency information. During this process, the specification sketch mechanism is introduced to guide the LLM in analyzing individual program segments and their dependencies, thereby structuring the subsequent generation process. Subsequently, the framework proceeds with iterative specification generation for each program segment, incorporating a novel mechanism for evaluating and refining specification semantic strength based on non-equivalent program mutations and variant discrimination. Guided by the insight that the semantic strength of specifications lies in their ability to distinguish programs from their non-equivalent variants, we measure the semantic strength of specifications by the number of variants they refute and leverage
Synthesis and Refinement of Formal Program Specifications
3
the assessment results to guide the LLM in generating stronger specifications. Eventually, the generated specifications for each segment are synthesized together to discharge a complete verification obligation for the target property. To comprehensively evaluate the performance of SpecSyn, we constructed a comprehensive benchmark consisting of 50 self-contained C source files retrieved from various open-source repositories, along with manually constructed ACSL specifications that are strong yet verifiable. Extensive experiments are conducted to compare SpecSyn against a series of state-of-the-art baseline approaches. Experimental results show that our method maintains a high level of precision from 90% to 100%, on par with state-of-the-art approaches, while achieving the highest average recall (over 75% on the majority of programs) among all baselines, which clearly demonstrates the effectiveness of the proposed approach. An ablation study is also conducted to prove the effectiveness of the divide-and-conquer design and the specification refinement mechanism. In further experiments on real-world program verification tasks, SpecSyn successfully discharges proof obligations for the most target properties (1071 out of 1365, compared to 503 of Preguss) among all baselines, revealing the practical applicability of our method and the effectiveness of the generated specifications in program verification tasks. The main contributions of this paper include: – A novel LLM-based framework for specification generation to support program verification, along with the corresponding prototype tool, which innovatively incorporates a specification strength evaluation and refinement mechanism based on non-equivalent program mutations and variant discrimination. – A dataset towards specification generation on real-world programs, containing C source code retrieved from real-world open-source repositories, together with strong yet verifiable ACSL specifications, facilitating follow-up research. – A comprehensive evaluation of SpecSyn and state-of-the-art baselines upon the proposed dataset, revealing the effectiveness of SpecSyn and the applicability of its generated specifications on verification tasks for real-world programs.
2
Background and Motivation
2.1
Program Specification Generation and Verification
Program specifications are precise statements that articulate the intended or actual behaviors of a given program, either as a whole or in its individual components [53]. A substantial portion of program specifications is formulated in formal languages, typically using mathematical notation or Boolean expressions, to define the constraints governing program behavior rigorously. Various formal specification languages have been established for different programming languages. In this work, we primarily focus on the ANSI/ISO C Specification Language (ACSL) [17] specifically designed for C programs. Three basic types of specification statements in ACSL are of particular concern: requires, specifying the preconditions on function arguments to guarantee proper function execution; ensures, specifying the postconditions that must be conformed to after function execution; and loop invariant, identifying the properties that consistently hold before executing the loop body.
4
Lezhi Ma, Shangqing Liu, Yi Li, Qiong Wu, Han Wang, and Lei Bu
Benefiting from the syntactic parsability and semantic analyzability of formal languages, specification verifiers, such as Frama-C/WP [16] for ACSL, have been developed to validate the correctness of program specifications (i.e., whether the semantics articulated by the specifications are consistent with the program’s actual behaviors [52]) through static approaches such as theorem proving and SMT solving [27, 15, 25]. Program verification can be achieved by formalizing the desired properties (such as safety constraints and functional requirements of modules, typically defined by human experts) into formal specifications and then proving their correctness using specification verifiers. Nevertheless, it takes more than the target property itself to conclude a successful proof, since realworld programs typically involve multiple control-flow structures, such as loops, method calls, and recursions, which verifiers cannot handle directly. To prove the specifications for higher-level entities such as modules, it is necessary to formulate effective supporting specifications for all critical low-level functions relied on by them, including contracts (pre/post-conditions) for these functions and loop invariants for the loops within. In this work, we mainly focus on these supporting specifications targeting the program’s actual behavior. This phenomenon imposes a substantial burden on software developers and domain experts, as formal specifications are highly intricate, subject to strict syntactic and semantic constraints, making their comprehension and construction tasks considerably time-consuming, eventually inhibiting the applicability of program specifications and their verification in real-world repositories. To alleviate this burden, a long stream of approaches for program specification generation has been proposed, ranging from traditional rule-based methods [33, 32, 54] and learning–based techniques [48, 68, 67] to the more recently emerging approaches [76, 53, 75] leveraging Large Language Models (LLMs) [59, 14, 60, 49, 38, 37]. 2.2
Motivation
Despite the significant advancements in program specification generation approaches brought about by LLMs, existing techniques still suffer from a range of limitations, hindering their applicability to real-world program verification tasks. Some methods, such as AutoSpec [76] and SpecGen [53], treat the input program holistically, typically presenting the entire program as the target of generation within the context provided to LLMs. This practice has a markedly negative impact on the scalability of the corresponding technique, not only due to the inherent constraint of limited context window sizes on LLMs, but also because of the attention dispersion problem [56], where LLM’s ability to distinguish informative tokens declines as the scale of input tokens expands, thereby degrading their performance on specification generation tasks. Moreover, existing approaches are primarily driven by the primitive objective of generating specifications that can pass verification, while lacking mechanisms to evaluate and enhance specification strength, i.e., whether a set of specifications precisely captures the characteristic behaviors of the target program rather than expressing trivial properties that hold for almost any program. Consequently, the strength of the generated specifications is not effectively guaranteed, which hinders the application of such specifications and the corresponding generation methods.
Synthesis and Refinement of Formal Program Specifications Input Program
5
RTE-guided Generation ①
①
②
②
③ ③
④
①
Naïve Hierarchical Generation
② ④ ④ ①
SpecSyn
②
③
④
Fig. 1. An example program segment from open-source repository X509-parser, the program specifications generated by each baseline method, and the corresponding verification results for the target property. ⃝∼ 1 ⃝ 3 marked three program points of interest where specifications should be generated, i.e., pre/post-conditions for the two functions and loop invariants for the loop within. ⃝ 4 marked the target property, on which the verification relies on the aforementioned specifications.
One illustrative example of these limitations is presented in Fig. 1, where state-of-the-art approaches [76, 75] showcase under-satisfactory performance in different aspects. Some approaches are essentially RTE-driven [75], focusing solely on memory readability and failing to generate effective postconditions for the essential functionalities of the function, which impairs the strength of the generated specifications and causes the verification failure of the target property. Other approaches adopt plain hierarchical strategies [76] when instructing LLMs to generate specifications, without effective repairing or refinement mechanisms, which yields a limited function contract and few meaningful loop invariants due to the attention dispersion problem, with the postcondition unprovable owing to insufficient loop invariants, let alone the verification target. These limitations pose a core challenge on the specification generation task: how to generate precise and useful specifications from sizable programs, so that the verification of target properties can be effectively supported? Confronted with the aforementioned challenge, we innovate SpecSyn, a novel technique featuring the synthesis and refinement of formal specifications for program verification, aiming to tackle the limitations of existing approaches ac-
6
Lezhi Ma, Shangqing Liu, Yi Li, Qiong Wu, Han Wang, and Lei Bu Top-down Task Decomposition and Analysis
Bottom-up Contract Synthesis Feedback
</> Input Program
//@
//@ Verification Target
Generation LLM
Specification Sketch
Proof
Intermediate Specification
Verifier //@
Dependency Analysis
Dependency Information
Planning LLM
//@
</> </> </>
Verifier
Mutated Segment
Feedback
Dependency Graph
SCC Extraction
</>
</> </> </>
Program Segments
Program Segment
Semantic-non-equivalent Mutation
Verifier
//@
//@ //@ //@
Segment Specification
Program Specification
Fig. 2. Overview of SpecSyn.
cordingly. To alleviate the input scale burden of real-world programs, we introduce Top-down Task Decomposition and Bottom-up Specification Synthesis, breaking down the enormous generation task to accomplish it in a divide-andconquer manner. To strengthen the semantics of the generated specifications, we introduce a specification strength assessment and refinement technique based on semantic-non-equivalent program mutation and variant discrimination. Benefited from the introduced designs, SpecSyn succeeded in summarizing comprehensive contracts and invariants for all crucial program points as demonstrated in Fig. 1, laying a solid foundation for the verification of the target property.
3
Methodology
3.1
Overview
The overview of our proposed approach, SpecSyn, is presented in Fig. 2. Taking as input the source code and the verification targets (expressed as ACSL specifications), our approach begins with Top-down Task Decomposition and Analysis (detailed in section 3.2), where existing static analysis techniques are first employed to construct a dependency graph. Program segments are then formulated as the minimal elements for specification generation and verification by identifying the strongly connected components of the dependency graph. Each program segment, together with its dependencies, is reasoned about by the planning LLM in turn to produce specification sketches for further guidance. Subsequently, our approach performs Bottom-up Specification Synthesis (detailed in section 3.3), in which each program segment is generated through an iterative generation process. After resolving the verification errors, we further incorporate a specification strength evaluation and refinement mechanism (detailed in section 3.4) based on semantic-non-equivalent mutations performed on the program segment, which strengthens the semantic expressiveness of the specifications and thereby supports the verification of the target properties. Eventually, specifications for all segments are summarized, upon which final verification is conducted to formulate a complete proof of the target properties.
Synthesis and Refinement of Formal Program Specifications
3.2
7
Top-down Task Decomposition and Analysis
Program Segmentation. Divide and conquer is a classical paradigm for tackling large-scale problems. When program specifications are to be generated for a large codebase, an intuitive strategy is to decompose it into smaller program segments and process them individually, thereby reducing the amount of input provided to the LLM in each invocation and alleviating the attention dispersion problem discussed above. Specifically, we begin by extracting all declarations and definitions within the input source code, including function definitions, user-defined type definitions, and free variable declarations, through the construction of an Abstract Syntax Tree (AST). The reference relations among these structures are then identified to formulate a dependency graph. To avoid circular dependencies among these structures, we subsequently apply Tarjan’s algorithm [71] to identify the strongly connected components (SCCs) of the dependency graph, and the corresponding program structures of each SCC as a decomposed segment. Each segment is regarded as a minimal element for generation and verification. The dependency information between these segments, i.e., which other segments’ contexts are necessary for verifying a given segment, is also summarized according to the dependency graph for further use. It is worth noting that, due to the characteristics of Tarjan’s algorithm, the produced sequence of program segments naturally respects a topological order, i.e., any segment depended upon will always appear before the segments that rely on it. Consequently, dependency conflicts are inherently avoided by processing the program segments sequentially according to this order. Specification Sketch Generation. To better coordinate the specification generation task across the entire program, we introduce a novel mechanism, namely the specification sketch. For each program segment, we provide its content and dependency information to a planning LLM, querying the model to generate a specification sketch, where the model is instructed to analyze and comprehend (in natural language) both the semantic content of the segment itself and its dependencies on other segments, enabling the model to plan the plausible form, syntax structure, and semantic content of the specification to generate, thereby guiding the subsequent specification generation tasks. A simplified prompt for sketch generation is listed as follows. Simplified Prompt for Specification Sketch Generation Consider the following C program segment: ```{code}``` Your task is to generate a specification sketch for this segment, describing and analyzing the corresponding specifications for the target program. Note that: 1. Identify all points of interest in the segment, and analyze the expected number, type, and semantics of specifications for each target location. 2. Be as specific as possible in the analysis, incorporating details on code semantics and specification functionalities. 3. Take special care of the dependency relationships between the specifications and the necessities to establish verifications on higher-level specifications. You might need the following code segments as dependencies: ```{code_dependency }```
An illustrative example for a specification sketch is presented in Fig. 3. Towards the three assertions instrumented in the code as verification targets, LLM
8
Lezhi Ma, Shangqing Liu, Yi Li, Qiong Wu, Han Wang, and Lei Bu
SpecSyn: Your task it to generate specification sketch for this code segment. Note that ……
Model: Below is a specification sketch for the given C segment.
Fig. 3. An example of a specification sketch towards the proof of verification targets.
automatically performs targeted planning for the preconditions and loop invariants required to support the verification. In the subsequent process, the model follows this plan to produce the structured specifications for discharging proof obligations towards the targets. This mechanism is inspired by the practice of planning in LLM-based agents, which can enhance the model’s comprehension towards the assigned task, reduce the risk of hallucinations, and improve the fault tolerance of the LLMs [40, 74]. Under the scenario of specification generation and program verification, the mechanism enables the model to reason about the program, verification targets, and corresponding specifications from an interprocedural perspective during the generation process, rather than focusing solely on the content of an individual program segment, facilitating the preservation of semantic coherence and relevance among the specifications generated for different segments. 3.3
Bottom-up Program Specification Synthesis
After formulating the set of code segments decomposed from the input program, SpecSyn proceeds to generate specifications for each segment and synthesize the generated specifications to formulate the complete specifications for the entire input program. Algorithm 1 presents a detailed illustration of the full synthesis procedure. The algorithm takes as input a dependency graph G of which the vertices are decomposed program segments and the edges are dependency relations, hyperparameter H specifying the max number of iterations allowed and a threshold for Variant Discrimination Guided Specification Refinement (detailed in section 3.4), an LLM M that outputs a set of specifications according to the given context, and a verifier V that reads a input program along with specifications and return a set of unprovable specifications. Generally, as described in function BottomUpSynthesis, the procedure handles each segment (expressed as the nodes v ∈ G.V within the dependency graph G) sequentially according to the aforementioned topological order, and eventually summarizes the specifications of each segment. Function GenSegmentSpecifications implements the process of handling a specific program segment. The function consists of three main components: Points of Interest Identification (line 9 in Alg. 1), Iterative Generation and Repairing (line 14∼21 in Alg. 1), and Variant Discrimination Guided Specification Refinement (line 22∼31 in Alg. 1, detailed in section 3.4).
Synthesis and Refinement of Formal Program Specifications
9
Algorithm 1: Bottom-up Program Specification Synthesis Input : Dependency graph G = ⟨V, E⟩ of program segments, Hyperparameter H = ⟨nref ine , nrepair , t⟩, Large Language Model M, verifier V Output: Set of program specifications S 1 Function BottomUpSynthesis(G, D, M, V) 2 S=∅ 3 for v ∈ G.V do 4 Sv = GenSegmentSpecifications(v, G, D, M, V) 5 S = S ∪ Sv 6
return S
Function GenSegmentSpecifications(v, G, D, M, V) 8 Sv = ∅ 9 for pos ∈ ExtractPointsOfInterest(v.code) do 10 Spos = ∅ 11 C = AssembleGenerationContext(v, pos, G) 12 i=0 13 repeat 14 j=0 15 repeat 16 Scand = M(C) 17 Sref uted = V(Scand , v.code) 18 Spos = ClearDuplicate(Spos ∪ (Scand \Sref uted )) 19 C = AssembleRepairContext(C, Sref uted ) 20 j =j+1 21 until Sref uted is ∅ or j ≥ H.nrepair ; 22 Pvariant = SemanticNonEquivalentMutate(v.code) 23 nref uted = 0 24 Ppassed = ∅ 25 for pvariant ∈ Pvariant do 26 if V(Spos , pvariant ) is not ∅ then 27 nref uted = nref uted + 1 7
else
28
Ppassed = Ppassed ∪ {pvariant }
29 30 31 32 33 34
C = AssembleRefineContext(C, Ppassed ) i=i+1 until nref uted /size(Pvariant ) ≥ H.t or i ≥ H.nref ine ; Sv = Sv ∪ Spos return Sv
Points of Interest Identification. Some existing approaches, e.g., SpecGen [53], allow the LLM to freely determine where to generate specifications by instructing the LLM to directly output all input source code instrumented with program specifications. Under this design, the model is not guaranteed to maintain the original syntactic and semantic structures of the input code due to hallucination, and specifications at critical locations may be omitted despite the instructions on the model to generate all necessary specifications. To avoid these deficiencies, we follow the same practice of AutoSpec [76], where a single location is explicitly specified each time for the LLM to generate corresponding specifications. To this end, before the iterative generation process, we first identify all points of interest (POI for short hereinafter) within the program segment, i.e., places where specifications should be generated and instrumented, including the beginning of function definitions and loops. It is worth noting that dependencies also exist among POIs. For instance, in the case of nested loops, verifying the invariants of the outer loop depends on the correctness of the invariant for the inner loop; for two sequential loops, the proof of invariants for the latter loop
10
Lezhi Ma, Shangqing Liu, Yi Li, Qiong Wu, Han Wang, and Lei Bu
depends on that of the former; and the proof of a function’s post-condition relies on the invariants of all loops within its body. To ensure a correct ordering of POIs, we perform a depth-first search on the segment’s AST to identify the relevant program structures, formulating a post-ordering sequence as the order of POIs. Dependency conflicts among POIs can thus be effectively eliminated. Iterative Generation and Repairing. For each POI, SpecSyn formulates a generation context (line 11 in Alg. 1) in preparation for further LLM query. The context consists of four main components: the previously generated specification sketch (introduced in section 3.2), the target program segment itself (with the target POI marked by a placeholder /* >>>INFILL<<< */), the instructions for the generation task, and the contents of the segments depended upon by the target segment. The context is thereby presented to the LLM to generate a set of candidate specifications (line 16 in Alg. 1). To distinguish between the correct and incorrect candidates, we verify all candidates against the program segment (with all necessary dependencies instrumented) using the verifier (i.e., Frama-C/WP [16]), which outputs a set of unproven candidates. According to the produced results, verified candidates are incorporated into the set of intermediate specifications (line 18 in Alg. 1) with duplicated candidates detected by lexical analysis and removed, whereas the refuted ones, along with the reported types of verification errors from the verifier, are utilized to construct a new query message that instructs the LLM to analyze and repair these errors. The model is thereby invoked repeatedly to generate a set of new candidates in substitution for the refuted ones. The process continues iteratively until no candidates are refuted or the maximum number of iterations is reached (line 21 in Alg. 1). 3.4
Variant Discrimination Guided Specification Refinement
The iterative generation and repairing process typically yields a set of verifiable specification statements. Naturally, one would wish that the generated specifications are semantically related to the target program closely for better support of program verification. Yet, unlike specification correctness, which can be determined relatively easily with the aid of a verifier, the semantic strength of specifications, i.e., how precise the statements are in terms of reflecting program behaviors [66], does not admit a rigorous definition and thus cannot be trivially assessed, resulting in the absence of mechanisms in existing approaches to guarantee the strength of generated specifications. To bridge this gap, we first propose a specification strength measurement technique based on program mutation and variant discrimination. The idea originates from the concept of trivial properties on programs, i.e., properties that either hold for all programs or fail to hold for all programs [69]. Similar intuitions can be adapted to program specifications as well: trivial specifications adapt to all programs, while non-trivial specifications hold for some programs but are rejected by others, i.e., they can distinguish programs with distinctive semantics. We expect the generated specifications to be more non-trivial and specific to the target program, so that they are more closely related in terms of semantics. Building on this insight, we propose the concept of variant discriminative rate to measure specification strength.
Synthesis and Refinement of Formal Program Specifications
11
Definition 1. Given a program p, a set of specification S, and a set M of semantic-non-equivalent mutation operators m : P → P , the variant discriminative rate (VDR) of S towards M is defined as P I(V(m(p), S) ̸= ∅) m∈M rv (S, p, M ) = |M | where V : P ×S → S is a verifier that takes as input a program p ∈ P and a set of specification S ∈ S to produce a set of refuted specifications, I : {true, false} → {0, 1} is the indicator function. Based on the definition of VDR, which acts as index for specification strength, we further formulate the task of VDR-guided specification refinement as follows: Definition 2. Given a program p ∈ P and a set M of non-equivalent mutation operators, VDR-guided specification refinement is an optimization problem to find a set of specifications S that S = arg min |M |(1 − rv (S, p, M )),
s.t. V(p, S) = ∅
S
where V : P × S → S is a verifier. We employ an iterative process driven by LLMs to address the optimization problem, eventually enabling the evaluation and refinement of specification strength. Generally, for the intermediate result Si obtained in each iteration, we iteratively optimize the results according to the formula below to yield a new set of specifications Si+1 : [ Si+1 = Si ∪ SM \ {s} s∈V(m(p),SM )
where
SM = M (p, Si , {m(p) | m ∈ M ∧ V(m(p), Si ) = ∅})
After obtaining a set Si of verifiable specifications for a given program segment, we apply semantic-non-equivalent mutations on the segment code to generate a collection of variants (line 22 in Alg. 1). The verifier then attempts to validate the specifications against each variant (line 25∼29 in Alg. 1), with both the number of variants that fail verification (distinguished) and those that pass (undistinguished) recorded. If the proportion of variants that fail verification exceeds a given threshold (line 32 in Alg. 1), the strength of the generated specifications is considered plausible. Otherwise, the undistinguished variants are utilized to construct a new query message (line 30 in Alg. 1), guiding the LLM in generating refined candidates. The message includes a randomly selected undistinguished variant and instructs the LLM to analyze the syntactic and semantic differences between this variant and the original program segment, and to propose new specifications for the properties that explicitly capture these differences. The approach then rolls back to the iterative generation and repairing procedure introduced (section 3.3) to ensure the verifiability of the new candidates.
12
Lezhi Ma, Shangqing Liu, Yi Li, Qiong Wu, Han Wang, and Lei Bu Input Program
Verifier: Passed!
Mutated Variant
Fig. 4. Illustration of specification refinement mechanism.
In terms of the mutation operators, we exploit the 188 mutation operators proposed by the work [61] targeting C compiler fuzzing. The operators are usefully comprehensive, covering a wide range of C language elements, including additions, removals, and modifications on operators, operands, identifiers, statements, control-flow structures, and user-defined type declarations. To ensure the semantic-non-equivalence of the mutations, we adopt Trivial Compiler Equivalence (TCE) [62], a lightweight technique for fast identification of program equivalence. The principle of TCE is to compile (usually with optimization flags specified) the programs to be assessed and consider them equivalent if the produced binary files are equal. We exploit the GNU C Compiler (GCC) [35] with the -O2 optimization flag specified to produce binary files for comparison. Mutated variant detected to be equivalent to the original segment will be excluded from the strength assessment process. An illustrative example of the refinement process is presented in Fig. 4. Despite some reasonable postconditions generated by LLM to specify the behavior of the function bufs_differ, these postconditions fail to impose proper bounds on the function’s return value. Semantically non-equivalent mutations on the program yield a variant in which the return value was altered. Since the intermediate specifications do not constrain the range of the return value, they still adapt to the variant. With this information as feedback, the model analyzes the discrepancy and identifies the need for explicit constraints. It then generated refined specifications that complemented this missing constraint, thereby strengthening the overall postcondition.
4
Experimental Setup
We aim to answer the following research questions through experiments: – RQ1: How is the performance of SpecSyn on specification generation tasks compared to existing LLM-based approaches? – RQ2: How do task decomposition and mutation-based refinement within SpecSyn contribute to its overall performance? – RQ3: How effective is SpecSyn along with its generated specifications when applied to real-world program verification tasks?
Synthesis and Refinement of Formal Program Specifications
4.1
13
Implementation
We implement the prototype of SpecSyn in Python for convenient access to LLM interfaces. Three models, including GPT-4 (version gpt-4-turbo-2024-04-09), GPT-5 (version gpt-5-2025-08-07), and DeepSeek-R1, are involved in the experiments. For GPT-4, temperature is set to 0 to improve performance on coding and reasoning tasks, with other settings identical to the default. For GPT-5 and Deepseek-R1, we adopt the default configuration. Frama-C/WP [16] 25.0 is adopted as the specification verifier. As for the hyperparameter mentioned in Alg. 1, we adopt the setting where nref ine = nrepair = 5 and t = 0.75. 4.2
Baselines
We compare SpecSyn against the following state-of-the-art LLM-based approaches: – Preguss [75], a specification generation approach featuring the guidance of potential runtime errors (RTEs) extracted by abstract interpretation. – AutoSpec [76], one of the first specification generation approaches that utilizes LLMs to generate candidate specifications. – SpecGen [53], a specification generation approach featuring heuristic mutations performed on the candidate specifications to fix semantic errors. – llama3.1-8b-instruct-fma and qwen2.5-coder-7b-instruct-fma, models fine-tuned by Cao et al. [21] on data corpora related to program specifications. 4.3
Benchmark Construction
RQ1&2. Currently, datasets and benchmarks for strong and verifiable ACSL specifications are remarkably limited. Despite the existence of certain datasets [7, 4] for toy examples, the programs contained are usually small in scale (typically cannot exceed 50 LoC per program), and the verifiability of the specifications provided is not strictly guaranteed, making them inadequate for reflecting the performance of baselines on real-world programs. To support the comprehensive evaluation of the baseline methods, we extracted a series of self-contained C source files from the following real-world open-source repositories: – UAV-Quadcopter [12], a controlling system for UAV based on Arduino. – voronoi [6], Voronoi diagram generation tool using Fortune’s algorithm [34]. – Hypatia [42], a low earth orbit satellite network simulation framework. – sokol [3] and CGL [5], development kits targeting WebAssembly. – BlueShiftEngine [10], Maratis [26], and Punity [8], rendering engines for demo construction and game development. – ccan [11], clib [2], zpl [13], and stb [9], third-party public domain libraries for utilities covering multiple areas. Apart from these programs, we also utilize the following established specifications among existing works: X509-parser [1], an RTE-free parser for X.509 certificates [19], and Java-JML [58], a set of Java programs with verifiable JML
14
Lezhi Ma, Shangqing Liu, Yi Li, Qiong Wu, Han Wang, and Lei Bu
specifications. A total of 50 programs were eventually collected, and we manually crafted strong yet verifiable ACSL specifications as ground truth. Detailed statistics of the programs are presented in Appendix ??. RQ3. Further evaluation of the applicability of baseline methods on software verification tasks necessitates programs with corresponding verification targets. We selected 3 files from voronoi [6], Hypatia [42], and sokol [3] and manually constructed verification targets (as ACSL assertions instrumented) from relevant documentation and test suites retrieved from these repositories. Apart from these repositories, we also utilize source files from X509-parser [31], Contiki [65], and Atomthreads [18], with RTE-related assertions retrieved from Preguss [75] artifact as targets. Additionally, we adopt the 220 programs in SV-COMP Benchmark (Reachability category), summarized by Cao et al. [21], in which the original assertions are already translated into ACSL statements. 4.4
Metrics
To comprehensively evaluate the quality of the generated specifications in terms of both correctness and strength, we follow the settings of previous works [55, 54] and evaluate the performance of baseline methods through the following metrics. – Precision, defined by the percentage of verifiable specifications over all generated specifications, measuring the correctness of the generated specifications. – Recall, defined by the percentage of ground-truth specifications covered by the generated specifications over all ground-truth specifications, measuring the strength of the generated specifications.
5
Experimental Results
5.1
RQ1: Overall Performance of Specification Generation
Table 1 shows the quality (correctness measured by precision, and strength measured by recall, both in percentages) of the specifications generated by each baseline method on the constructed dataset. Specification Correctness. Overall, SpecSyn incorporating GPT-5 yields the highest average precision (96.68%) among all baseline approaches. The following baseline approach is Preguss, with both the GPT-5 and GPT-4 versions yielding a precision above 93%. Both approaches are equipped with effective mechanisms to filter out incorrect specifications according to the feedback of the verifier, guaranteeing the correctness of the generated specifications. Consequently, the difference in precision between the two methods is not substantial. In contrast to these methods, the remaining approaches suffer from a substantial degradation in precision. SpecGen achieves 83.37% precision, while AutoSpec only yields 66.94%. As claimed in section 2.2, these two approaches treat the input program holistically, loading the entire program into LLMs’ context, which hinders the performance of LLMs and the quality of generated specifications. Specifically, for programs over 500 LoC, AutoSpec is only able to generate specifications for a
Synthesis and Refinement of Formal Program Specifications
15
Table 1. Performance of each baseline method on the specification generation task. Prec.: precision, Rec.: recall, both in percentages. X509- JavaUAVvoronoi hypatia sokol parser JML Quadcopter
Repository Average LoC per File GPT-5
Prec. 95.66 97.80 Rec. 85.30 82.27
97.57 41.96
99.39 97.24 86.83 95.67
GPT-4
Prec. 98.61 98.37 Rec. 64.17 76.51
95.69 40.79
98.43 86.83
DS-R1
Prec. 96.11 96.07 Rec. 36.95 44.61
98.87 49.42
GPT-5
Prec. 33.33 84.72 Rec. 9.52 28.21
GPT-4
553
350
550
632
zpl
stb 299
Avg.
99.13 98.77 99.24 90.94 86.88 99.31 96.68 84.53 47.37 80.58 77.43 73.48 61.62 75.91
73.81 81.10
89.29 100.00 79.21 100.00
93.91 77.91
97.15 56.86
95.95 98.89 95.49 91.08 96.61 94.52 80.70 66.19 61.99 66.29 56.89 71.10
93.34 83.83
89.74 92.91
99.13 100.00 33.65 100.00
94.67 56.80
98.80 58.48
91.88 98.76 93.12 92.79 97.86 95.80 57.89 61.49 58.22 63.98 58.57 61.20
100.00 15.85
80.00 31.62
95.24 1.57
81.25 6.72
42.86 66.67
85.40 10.31
16.67 0.84
90.00 66.67 79.39 81.67 0.00 66.94 14.04 11.98 21.56 11.87 0.00 16.48
Prec. 74.21 78.71 Rec. 33.86 26.31
50.00 15.85
69.55 34.62
94.59 28.35
37.50 1.32
40.85 29.17
75.43 26.60
80.00 21.00
45.77 81.11 71.60 47.94 81.03 66.31 5.26 41.47 16.54 10.55 18.75 22.12
GPT-5
Prec. 75.97 76.50 Rec. 43.46 68.20
53.85 15.38
100.00 69.67 77.12 51.97
91.89 100.00 81.80 100.00
90.58 79.73
97.67 58.06
93.85 69.84 78.63 80.05 88.71 83.37 68.42 44.19 50.45 61.24 43.19 60.23
GPT-4
Prec. 92.21 75.84 Rec. 32.06 42.94
50.00 14.69
90.68 84.29
98.51 61.42
0.00 0.00
100.00 100.00
12.50 8.70
89.81 48.28
98.25 91.07 80.63 66.52 70.73 72.62 82.46 45.26 35.76 38.77 34.54 44.94
GPT-5
Prec. 66.67 95.78 Rec. 10.27 29.15
99.54 35.43
100.00 36.11
99.13 53.15
99.00 13.85
90.00 33.33
100.00 21.17
97.38 32.76
97.96 81.98 96.56 89.73 98.15 93.70 24.56 36.42 38.68 36.44 28.69 30.72
GPT-4
Prec. 66.67 98.09 Rec. 15.61 24.85
99.28 35.66
100.00 100.00 100.00 100.00 23.73 34.25 15.16 37.50
100.00 32.14
97.53 27.14
98.25 83.33 96.37 86.56 92.82 94.21 22.81 24.76 28.93 27.93 25.56 26.86
llama3.1-fma
Prec. 25.24 26.75 Rec. 0.00 11.97
0.00 0.00
0.00 0.00
0.00 0.00
21.55 10.81
0.00 0.00
0.00 0.00
0.00 0.00
0.00 0.00
0.00 0.00
0.00 0.00
0.00 0.00
0.00 0.00
5.25 1.63
qwen2.5-fma
Prec. 0.00 Rec. 0.00
0.00 0.00
0.00 0.00
0.00 0.00
0.00 0.00
0.00 0.00
0.00 0.00
0.00 0.00
0.00 0.00
0.00 0.00
0.00 0.00
0.00 0.00
0.00 0.00
0.55 0.20
7.74 2.73
1323
524
98.18 73.09
Preguss
348
551
93.42 100.00 76.77 95.83
SpecGen
1741
clib
732
AutoSpec
207
BlueShift Maratis Punity ccan Engine 358
SpecSyn
95
cgl
handful of functions, and the output content of the incorporated LLM typically suffers from serious syntax errors. The remaining two fine-tuned models, lama3.18b-instruct-fma and qwen2.5-coder-7b-instruct-fma, can only generate limited meaningful content on the input programs and thus yield marginal precision. The two models are fine-tuned on relatively small-scale (7B∼8B) base models, which inherently cannot handle sizable input effectively. Specification Strength. Generally, SpecSyn incorporating GPT-5 yields the highest average recall (75.91%) on all programs adopted in the experiments, significantly outperforming all other baselines involved. Other versions of SpecSyn incorporating GPT-4 and Deepseek-R1 also demonstrate considerable performance, achieving 71.10% and 61.20% recall, respectively. Notably, for 13 repositories among the 14 involved in the experiments, the highest average recall is witnessed on the different versions of SpecSyn. The result indicates the remarkable semantic strength of the specifications by SpecSyn, benefiting from the innovative mechanism for specification refinement based on program mutation and variant discrimination. Apart from SpecSyn, the best-performing approach is SpecGen incorporating GPT-5. In comparison, Preguss can only achieve a relatively limited recall of around 30%. Preguss places excessive emphasis on RTE guidance, which is strongly related to preconditions but has only an indirect influence on postconditions and loop invariants, and thus fails to provide strong and effective guidance when it comes to these two types of specifications, adversely affecting their quantity and quality. AutoSpec is constrained by the LLM’s attention dispersion problem and consequently yields only around 20% recall. The recall of the two fine-tuned models remains exceptionally low due to the aforementioned scalability problem of small-scale models.
16
Lezhi Ma, Shangqing Liu, Yi Li, Qiong Wu, Han Wang, and Lei Bu Table 2. Performance of SpecSyn with main components disabled respectively. Repository Average LoC
X509- JavaUAVvoronoi hypatia sokol parser JML Quadcopter 207
1741
348
Prec. 95.66 97.80 Rec. 85.30 82.27
97.57 41.96
w/o Prec. 84.09 80.90 decomposition Rec. 73.57 69.10
SpecSyn
w/o refinement
5.2
95
Prec. 98.08 97.64 Rec. 84.23 81.04
1323
553
cgl 350
BlueShift Maratis Punity ccan Engine 550
632
clib
zpl
stb
551
524
299
Avg.
358
732
99.39 97.24 93.42 100.00 86.83 95.67 76.77 95.83
98.18 73.09
99.13 98.77 99.24 90.94 86.88 99.31 96.68 84.53 47.37 80.58 77.43 73.48 61.62 75.91
82.86 18.65
75.40 84.29
85.99 56.30
83.75 96.49 68.76 91.67
88.96 76.00
92.13 77.07
92.21 87.26 79.15 81.28 83.56 85.29 52.63 59.47 61.34 61.32 35.26 63.25
99.51 39.63
99.31 85.14
96.54 77.95
90.37 98.80 75.89 91.67
95.82 58.20
98.01 83.01
98.42 95.07 80.10 79.27 97.86 94.63 57.89 70.99 56.84 65.04 60.42 70.57
RQ2: Ablation Study
We further conduct an ablation study to evaluate the effectiveness of the main components within SpecSyn. The results are shown in Table 2 where w/o {*} denotes the variant of SpecSyn with the corresponding component disabled. All variants incorporate GPT-5 for generation. When the divide-and-conquer design is disabled, i.e., without the top-down decomposition and the bottom-up synthesis process, both the precision and recall metrics of SpecSyn exhibit a noticeable decline, with the precision dropping by 11.41% and recall dropping by 12.66%. This is due to the increasing burden on model attention as the input program scale grows. On some sizable programs, e.g., the 1741 LoC file from UAV-quadcopter, the degradation of model performance is particularly sharp, with the recall metric dropping by 23.31%. When the specification refinement mechanism is removed, SpecSyn experiences an average decrease of approximately 2% in precision and about 5% in recall. Since the specification refinement mechanism is primarily designed to guide the model toward generating semantically stronger specifications, its contribution is manifested more prominently in recall than in precision. Given that SpecSyn incorporating GPT-4 and the refinement mechanism achieves a recall of 71.10% (Table 1), which is comparable to the performance obtained when using GPT-5 yet with the refinement mechanism disabled, we may conclude that the refinement mechanism contributes sufficiently to the strength of the generated specifications so as to compensate for the capability gap between the GPT-4 and GPT-5 models. 5.3
RQ3: Applications on Real-world Software Verification Tasks
Table 3 shows the number of verification targets successfully proved by FramaC/WP with the support of the specifications generated by each baseline method. Generally, the programs involved consist of the following three categories. Voronoi, Hypatia, and Sokol. Constructed according to the software documentation and test suites of the original repositories, the targets within these programs encompass a wide spectrum of categories, including checks on variable values, boundary conditions, pointer reference validity, and universal/existential property assertions. Proof obligations for these targets necessitate a relatively comprehensive summarization of program functionalities and behaviors. On these programs, our method demonstrates outstanding performance, successfully discharging obligations for around 90% verification targets for each program. This benefits from the specification refinement mechanism and the
Synthesis and Refinement of Formal Program Specifications
17
Table 3. Number of proved target properties by each baseline method. Repository
voronoi Hypatia sokol X509-parser Contiki Atomthreads SVCOMP Total
Avg. LoC per File Number of Targets
424 172
1323 195
821 241
1199 142
544 163
1451 239
27.79 220
1365
SpecSyn Preguss AutoSpec llama3.1-fma
153 39 19 9
187 15 22 0
220 31 13 14
132 125 37 0
73 103 24 0
130 108 1 0
132 82 10 6
1071 503 126 29
strong specifications produced, which can precisely capture the essential behaviors and functionalities of the input programs, formulating a solid foundation for verification of target properties. In contrast, Preguss is able to discharge only 10%∼25% of the proof obligations, as its generation process focuses solely on RTEs, leading to insufficient generality in the generated specifications. Suffering from the scalability problem introduced in section 2.2, AutoSpec and llama3.1-8b-instruct-fma can only generate a limited number of meaningful specifications, struggling to support the verification process. X509-parser, Contiki, and Atomthreads. The programs in these repositories are retrieved from the Preguss artifact [75], which is RTE-oriented during generation, and the corresponding targets are primarily assertions that exclude RTEs from execution. Preguss demonstrates considerable capability in handling these targets, generating specifications that successfully support the verification for the majority of targets by meticulously handling the inference of appropriate preconditions. In comparison, without applying any specialized mechanism towards RTE, SpecSyn still achieves performance comparable to Preguss, successfully yielding more proof obligations for 2 of the 3 programs. This benefits from the specification sketch introduced in section 3.2, where LLM identifies the assertions instrumented in the input code and plans their verification in advance. SV-COMP. Most programs in the SV-COMP benchmark are relatively small in scale (27.79 LoC on average for the programs adopted for experiments) and rarely involve function calls, with their verification primarily relying on appropriate loop invariants rather than interprocedural specifications. Upon these programs, SpecSyn still showcases leading performance among all baseline methods, successfully discharging verification obligations for 132 targets. In contrast, Preguss’s capability in inferring loop invariants can only help verify a limited subset of targets. Despite the significant reduction in the size of the input programs, the specifications generated by AutoSpec and llama3.1-8b-instruct-fma remain largely insufficient to support the verification of the target properties, since their design does not take proof obligation production into consideration.
6
Limitations
The main limitation of the proposed framework lies in its computational cost in terms of execution time. Since the specification refinement mechanism requires validating each program variant against the target specifications, it entails repeated invocations of the verifier, thereby incurring a significant increase in the
18
Lezhi Ma, Shangqing Liu, Yi Li, Qiong Wu, Han Wang, and Lei Bu
overall runtime. On the 50 source files adopted in the dataset constructed, Preguss consumes on average 1.42 hours to handle one source file, while it takes 3.62 hours for SpecSyn, which is approximately 2.5 times longer than Preguss. The limitation can be alleviated by refining the framework implementation, such as introducing concurrent computing into the refinement mechanism, or by incorporating more computational resources.
7
Related Works
Program Mutation for Testing. One typical use of program mutations is mutation-based testing, a technique for measuring the effectiveness of a test suite by assessing its ability to detect potential faults [41, 63]. The operators typically involve only simplistic modifications targeting only a single program point [23, 73, 72]. Apart from mutation-based testing, program mutations also play a vital role in compiler fuzzing. Conventional compiler fuzzing techniques typically rely on manually crafted mutation operators [45, 46, 70]. With the rise of LLMs, recent works have proposed diverse fuzzing approaches incorporating LLMs into the program mutation process [28, 61, 57]. LLM-based Specification Generation. Conventional approaches of program specification generation typically rely on heuristic rules [33, 32, 54], static analysis techniques [44, 20, 29, 24, 39], and learning-based techniques [48, 51, 43, 36, 67, 68]. Apart from these approaches, the recent emergence and widespread adoption of LLMs have brought about a comprehensive transformation in the field of specification generation. AutoSpec [76] first incorporates LLMs into specification generation tasks and utilizes static analysis to identify code hierarchy as guidance to LLMs. SpecGen [53] introduces conversational generation and heuristic mutation operators in an attempt to repair verification errors of LLM-generated results. Pei et al. [64] and Cao et al. [21] aim to improve the performance of LLMs on specification generation tasks by fine-tuning them on data corpora related to program specifications. Compared to these works that treat the input program holistically, SpecSyn handles the input program in a divide-and-conquer manner, enhancing the scalability of the approach. Preguss [75] incorporates abstract interpretation to extract potential runtime errors (RTE), guiding the LLM to generate specifications that exclude these errors. Compared to this work, which focuses solely on RTE-related specifications, SpecSyn adopts a more versatile perspective, independent of the target specification’s type, and can generate specifications that characterize the essential behaviors and functionalities of the input program. Other works [22, 50, 77, 78] also target Verus specifications for Rust code and PSL for smart contracts, incorporating techniques such as multiagent network and retrieval-augmented generation. Due to intractable differences in terms of target programming language, specification language, and the corresponding verifier, these works are excluded from the experiments for comparison.
8
Conclusion
This paper presents SpecSyn, a novel LLM-based specification generation approach. SpecSyn incorporate top-down decomposition and bottom-up synthesis
Synthesis and Refinement of Formal Program Specifications
19
to enhance the framework’s scalability, while incorporating an innovative specification refinement mechanism based on program mutations and variant discrimination. Experimental results demonstrate the quality of specifications generated by SpecSyn, the effectiveness of the innovated specification refinement mechanism, and the applicability of SpecSyn on real-world verification tasks.
References 1. GitHub ANSSI-FR/x509-parser: a RTE-free X.509 parser. https://github.com/ANSSI-FR/x509-parser (2026) 2. GitHub - clibs/clib: Package manager for the C programming language. https://github.com/clibs/clib (2026) 3. GitHub - floooh/sokol: minimal cross-platform standalone C headers. https://github.com/floooh/sokol (2026) 4. GitHub - fraunhoferfokus/acsl-by-example: Public snapshots of "ACSL by Example". https://github.com/fraunhoferfokus/acsl-by-example (2026) 5. GitHub - Jaysmito101/cgl: CGL (C Game Library) is a multipurpose library mainly for recreational coding / demo scenes / prototyping / small games / experimentation. https://github.com/Jaysmito101/cgl (2026) 6. GitHub - JCash/voronoi: A C implementation for creating 2D voronoi diagrams. https://github.com/JCash/voronoi (2026) 7. GitHub - manavpatnaik/frama-c-problems: A repository dedicated for problems related to verification of programs using the tool frama-c. https://github.com/manavpatnaik/frama-c-problems (2026) 8. GitHub martincohen/Punity: A tiny game engine in C. https://github.com/martincohen/Punity (2026) 9. GitHub - nothings/stb: stb single-file public domain libraries for C/C++. https://github.com/nothings/stb (2026) 10. GitHub - PolygonTek/BlueshiftEngine. https://github.com/PolygonTek/BlueshiftEngine (2026) 11. GitHub rustyrussell/ccan: The C Code Archive Network. https://github.com/rustyrussell/ccan (2026) 12. GitHub - SHRC/UAV-Quadcopter: Program for Arduino-Controlled UAV Quadcopter. https://github.com/SHRC/UAV-Quadcopter (2026) 13. GitHub - zpl-c/zpl: Pushing the boundaries of simplicity. https://github.com/zplc/zpl (2026) 14. Achiam, J., Adler, S., Agarwal, S., Ahmad, L., Akkaya, I., Aleman, F.L., Almeida, D., Altenschmidt, J., Altman, S., Anadkat, S., et al.: Gpt-4 technical report. arXiv preprint arXiv:2303.08774 (2023) 15. Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanović, D., King, T., Reynolds, A., Tinelli, C.: cvc4. In: International Conference on Computer Aided Verification. pp. 171–177. Springer (2011) 16. Baudin, P., Bobot, F., Correnson, L., Dargaye, Z., Blanchard, A.: WP Plug-in Manual, https://frama-c.com/download/frama-c-wp-manual.pdf 17. Baudin, P., Filliâtre, J.C., Marché, C., Monate, B., Moy, Y., Prevosto, V.: Acsl: Ansi c specification language. CEA-LIST, Saclay, France, Tech. Rep. v1 2, 79 (2008) 18. Beyer, D., Strejček, J.: Improvements in software verification and witness validation: Sv-comp 2025. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems. pp. 151–186. Springer (2025)
20
Lezhi Ma, Shangqing Liu, Yi Li, Qiong Wu, Han Wang, and Lei Bu
19. Boeyen, S., Santesson, S., Polk, T., Housley, R., Farrell, S., Cooper, D.: Internet X.509 Public Key Infrastructure Certificate and Certificate Revocation List (CRL) Profile. RFC 5280 (May 2008). https://doi.org/10.17487/RFC5280, https://www.rfc-editor.org/info/rfc5280 20. Calcagno, C., Distefano, D., Vafeiadis, V.: Bi-abductive resource invariant synthesis. In: Asian Symposium on Programming Languages and Systems. pp. 259–274. Springer (2009) 21. Cao, J., Lu, Y., Li, M., Ma, H., Li, H., He, M., Wen, C., Sun, L., Zhang, H., Qin, S., et al.: From informal to formal–incorporating and evaluating llms on natural language requirements to verifiable formal proofs. arXiv preprint arXiv:2501.16207 (2025) 22. Chen, T., Lu, S., Lu, S., Gong, Y., Yang, C., Li, X., Misu, M.R.H., Yu, H., Duan, N., Cheng, P., et al.: Automated proof generation for rust code via self-evolution. arXiv preprint arXiv:2410.15756 (2024) 23. Coles, H., Laurent, T., Henard, C., Papadakis, M., Ventresque, A.: Pit: a practical mutation testing tool for java. In: Proceedings of the 25th international symposium on software testing and analysis. pp. 449–452 (2016) 24. Colón, M.A., Sankaranarayanan, S., Sipma, H.B.: Linear invariant generation using non-linear constraint solving. In: International Conference on Computer Aided Verification. pp. 420–432. Springer (2003) 25. Conchon, S., Coquereau, A., Iguernlala, M., Mebsout, A.: Alt-ergo 2.2. In: SMT Workshop: International Workshop on Satisfiability Modulo Theories (2018) 26. Davide, B.: maratis3d.org. http://www.maratis3d.org/ (2026) 27. De Moura, L., Bjørner, N.: Z3: An efficient smt solver. In: International conference on Tools and Algorithms for the Construction and Analysis of Systems. pp. 337– 340. Springer (2008) 28. Deng, Y., Xia, C.S., Peng, H., Yang, C., Zhang, L.: Large language models are zero-shot fuzzers: Fuzzing deep-learning libraries via large language models. In: Proceedings of the 32nd ACM SIGSOFT international symposium on software testing and analysis. pp. 423–435 (2023) 29. Dillig, I., Dillig, T., Li, B., McMillan, K.: Inductive invariant generation via abductive inference. Acm Sigplan Notices 48(10), 443–456 (2013) 30. D’silva, V., Kroening, D., Weissenbacher, G.: A survey of automated techniques for formal software verification. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 27(7), 1165–1178 (2008) 31. Ebalard, A., Mouy, P., Benadjila, R.: Journey to a rte-free x. 509 parser. In: Symposium sur la sécurité des technologies de l’information et des communications (SSTIC 2019). vol. 186 (2019) 32. Ernst, M.D., Perkins, J.H., Guo, P.J., McCamant, S., Pacheco, C., Tschantz, M.S., Xiao, C.: The daikon system for dynamic detection of likely invariants. Science of computer programming 69(1-3), 35–45 (2007) 33. Flanagan, C., Leino, K.R.M.: Houdini, an annotation assistant for esc/java. In: International Symposium of Formal Methods Europe. pp. 500–517. Springer (2001) 34. Fortune, S.: A sweepline algorithm for voronoi diagrams. In: Proceedings of the second annual symposium on Computational geometry. pp. 313–322 (1986) 35. Foundation, F.S.: Gcc, the gnu compiler collection - gnu project (2026), https://gcc.gnu.org/ 36. Garg, P., Neider, D., Madhusudan, P., Roth, D.: Learning invariants using decision trees and implication counterexamples. ACM Sigplan Notices 51(1), 499–512 (2016)
Synthesis and Refinement of Formal Program Specifications
21
37. Grattafiori, A., Dubey, A., Jauhri, A., Pandey, A., Kadian, A., Al-Dahle, A., Letman, A., Mathur, A., Schelten, A., Vaughan, A., et al.: The llama 3 herd of models. arXiv preprint arXiv:2407.21783 (2024) 38. Guo, D., Yang, D., Zhang, H., Song, J., Zhang, R., Xu, R., Zhu, Q., Ma, S., Wang, P., Bi, X., et al.: Deepseek-r1: Incentivizing reasoning capability in llms via reinforcement learning. arXiv preprint arXiv:2501.12948 (2025) 39. Gupta, A., Rybalchenko, A.: Invgen: An efficient invariant generator. In: International Conference on Computer Aided Verification. pp. 634–640. Springer (2009) 40. Huang, X., Liu, W., Chen, X., Wang, X., Wang, H., Lian, D., Wang, Y., Tang, R., Chen, E.: Understanding the planning of llm agents: A survey. arXiv preprint arXiv:2402.02716 (2024) 41. Jia, Y., Harman, M.: An analysis and survey of the development of mutation testing. IEEE transactions on software engineering 37(5), 649–678 (2010) 42. Kassing, S., Bhattacherjee, D., Águas, A.B., Saethre, J.E., Singla, A.: Exploring the “Internet from space” with Hypatia. In: ACM IMC (2020) 43. Krishna, S., Puhrsch, C., Wies, T.: Learning invariants using decision trees. arXiv preprint arXiv:1501.04725 (2015) 44. Laviron, V., Logozzo, F.: Subpolyhedra: A (more) scalable approach to infer linear inequalities. In: International Workshop on Verification, Model Checking, and Abstract Interpretation. pp. 229–244. Springer (2009) 45. Le, V., Afshari, M., Su, Z.: Compiler validation via equivalence modulo inputs. ACM Sigplan Notices 49(6), 216–226 (2014) 46. Le, V., Sun, C., Su, Z.: Finding deep compiler bugs via guided stochastic program mutation. Acm Sigplan Notices 50(10), 386–399 (2015) 47. Leavens, G.T., Poll, E., Clifton, C., Cheon, Y., Ruby, C., Cok, D., Müller, P., Kiniry, J., Chalin, P., Zimmerman, D.M., et al.: Jml reference manual (2008) 48. Li, J., Sun, J., Li, L., Le, Q.L., Lin, S.W.: Automatic loop-invariant generation anc refinement through selective sampling. In: 2017 32nd IEEE/ACM International Conference on Automated Software Engineering (ASE). pp. 782–792. IEEE (2017) 49. Liu, A., Feng, B., Xue, B., Wang, B., Wu, B., Lu, C., Zhao, C., Deng, C., Zhang, C., Ruan, C., et al.: Deepseek-v3 technical report. arXiv preprint arXiv:2412.19437 (2024) 50. Liu, Y., Xue, Y., Wu, D., Sun, Y., Li, Y., Shi, M., Liu, Y.: Propertygpt: Llmdriven formal verification of smart contracts through retrieval-augmented property generation. arXiv preprint arXiv:2405.02580 (2024) 51. Lu, H., Wang, C., Gui, J., Huang, H.: Pblinv: Postcondition-based loop invariant learning for c programs. In: 2020 IEEE 20th International Conference on Software Quality, Reliability and Security (QRS). pp. 1–12 (2020). https://doi.org/10.1109/QRS51102.2020.00013 52. Ma, L., Liu, S., Bu, L., Li, S., Wang, Y., Liu, Y.: Speceval: Evaluating code comprehension in large language models via program specifications. arXiv preprint arXiv:2409.12866 (2024) 53. Ma, L., Liu, S., Li, Y., Xie, X., Bu, L.: Specgen: Automated generation of formal program specifications via large language models. arXiv preprint arXiv:2401.08807 (2024) 54. Molina, F., d’Amorim, M., Aguirre, N.: Fuzzing class specifications. In: Proceedings of the 44th International Conference on Software Engineering. pp. 1008–1020 (2022) 55. Molina, F., Ponzio, P., Aguirre, N., Frias, M.: Evospex: An evolutionary algorithm for learning postconditions. In: 2021 IEEE/ACM 43rd International Conference on Software Engineering (ICSE). pp. 1223–1235. IEEE (2021)
22
Lezhi Ma, Shangqing Liu, Yi Li, Qiong Wu, Han Wang, and Lei Bu
56. Mudarisov, T., Burtsev, M., Petrova, T., State, R.: Limitations of normalization in attention mechanism. arXiv preprint arXiv:2508.17821 (2025) 57. Munley, C., Jarmusch, A., Chandrasekaran, S.: Llm4vv: Developing llm-driven testsuite for compiler validation. Future Generation Computer Systems 160, 1–13 (2024) 58. Nilizadeh, A., Leavens, G.T., Le, X.B., Pasareanu, C.S., Cok, D.: Exploring true test overfitting in dynamic automated program repair using formal methods (in press). In: 2021 14th IEEE Conference on Software Testing, Validation and Verification (ICST). IEEE (2021) 59. OpenAI: Gpt-3.5 (2026), https://platform.openai.com/docs/models/gpt-3-5 60. OpenAI: Gpt-5 model (2026), https://platform.openai.com/docs/models/gpt-5 61. Ou, X., Li, C., Jiang, Y., Xu, C.: The mutators reloaded: Fuzzing compilers with large language model generated mutation operators. In: Proceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 4. pp. 298–312 (2024) 62. Papadakis, M., Jia, Y., Harman, M., Le Traon, Y.: Trivial compiler equivalence: A large scale empirical study of a simple, fast and effective equivalent mutant detection technique. In: 2015 IEEE/ACM 37th IEEE International Conference on Software Engineering. vol. 1, pp. 936–946. IEEE (2015) 63. Papadakis, M., Kintis, M., Zhang, J., Jia, Y., Le Traon, Y., Harman, M.: Mutation testing advances: an analysis and survey. In: Advances in computers, vol. 112, pp. 275–378. Elsevier (2019) 64. Pei, K., Bieber, D., Shi, K., Sutton, C., Yin, P.: Can large language models reason about program invariants? In: International Conference on Machine Learning. pp. 27496–27520. PMLR (2023) 65. Peyrard, A., Kosmatov, N., Duquennoy, S., Raza, S.: Towards formal verification of contiki: Analysis of the aes–ccm* modules with frama-c. In: RED-IOT 2018Workshop on Recent advances in secure management of data and resources in the IoT (2018) 66. Polikarpova, N., Furia, C.A., Pei, Y., Wei, Y., Meyer, B.: What good are strong specifications? In: 2013 35th international conference on software engineering (icse). pp. 262–271. IEEE (2013) 67. Ryan, G., Wong, J., Yao, J., Gu, R., Jana, S.: Cln2inv: learning loop invariants with continuous logic networks. arXiv preprint arXiv:1909.11542 (2019) 68. Si, X., Dai, H., Raghothaman, M., Naik, M., Song, L.: Learning loop invariants for program verification. Advances in Neural Information Processing Systems 31 (2018) 69. Sipser, M.: Introduction to the theory of computation. ACM Sigact News 27(1), 27–29 (1996) 70. Sun, C., Le, V., Su, Z.: Finding compiler bugs via live code mutation. In: Proceedings of the 2016 ACM SIGPLAN international conference on object-oriented programming, systems, languages, and applications. pp. 849–863 (2016) 71. Tarjan, R.: Depth-first search and linear graph algorithms. SIAM journal on computing 1(2), 146–160 (1972) 72. Wang, B., Chen, M., Lin, Y., Papadakis, M., Zhang, J.M.: An exploratory study on using large language models for mutation testing. arXiv preprint arXiv:2406.09843 (2024) 73. Wang, B., Lu, S., Xiong, Y., Liu, F.: Faster mutation analysis with fewer processes and smaller overheads. In: 2021 36th IEEE/ACM International Conference on Automated Software Engineering (ASE). pp. 381–393. IEEE (2021)
Synthesis and Refinement of Formal Program Specifications
23
74. Wang, L., Ma, C., Feng, X., Zhang, Z., Yang, H., Zhang, J., Chen, Z., Tang, J., Chen, X., Lin, Y., et al.: A survey on large language model based autonomous agents. Frontiers of Computer Science 18(6), 186345 (2024) 75. Wang, Z., Lin, T., Chen, M., Li, H., Yang, M., Yi, X., Qin, S., Luo, Y., Li, X., Gu, B., et al.: A tale of 1001 loc: Potential runtime error-guided specification synthesis for verifying large-scale programs. arXiv preprint arXiv:2512.24594 (2025) 76. Wen, C., Cao, J., Su, J., Xu, Z., Qin, S., He, M., Li, H., Cheung, S.C., Tian, C.: Enchanting program specification synthesis by large language models using static analysis and program verification. In: International Conference on Computer Aided Verification. pp. 302–328. Springer (2024) 77. Yang, C., Li, X., Misu, M.R.H., Yao, J., Cui, W., Gong, Y., Hawblitzel, C., Lahiri, S., Lorch, J.R., Lu, S., et al.: Autoverus: Automated proof generation for rust code. Proceedings of the ACM on Programming Languages 9(OOPSLA2), 3454– 3482 (2025) 78. Zhong, S., Zhu, J., Tian, Y., Si, X.: Rag-verus: Repository-level program verification with llms using retrieval augmented generation. arXiv preprint arXiv:2502.05344 (2025)