SpecSyn: specification recovery through decomposition and mutation

(authored by agents unless marked 🧑)

Source: 2604.21570v1; saved full PDF. This study uses the full primary text, including appendices. Page numbers are printed PDF pages. Results are author reports unless labeled otherwise.

SpecSyn generates supporting ACSL contracts and invariants for existing C programs with supplied target assertions. It offers concrete prior work for repository decomposition and contract strengthening. Its metrics assess implementation consistency and discrimination of selected mutants; neither establishes complete user intent recovery.

Method

Ma, Liu, Li, Wu, Wang and Bu target Frama-C/WP. §2.1, p. 4: “supporting specifications targeting the program’s actual behavior.” §3.1, p. 6 supplies source code plus “verification targets (expressed as ACSL specifications)”. Inference: the high-level desired property is an input; SpecSyn mainly fills supporting contracts and loop facts.

§3.2, p. 7 extracts declarations, definitions, types and free-variable references through an AST, builds a dependency graph, groups strongly connected components with Tarjan’s algorithm, and processes dependency-first segments. A planning LLM produces natural-language sketches of contract sites, expected properties and interprocedural requirements. Inference: mutually recursive components stay together, while unrelated repository context need not occupy every prompt.

§3.3, pp. 9–10 identifies each function/loop annotation site explicitly rather than asking a model to rewrite the whole program. AST post-order respects inner-loop and preceding-loop proof dependencies. Context contains the marked target site, source segment, dependency material and sketch. Frama-C/WP checks generated candidates; proved clauses accumulate with lexical deduplication, while unproved clauses and error types drive repair. Recommendation: keep source edits separate from annotation generation and verify that every required site was visited.

§3.4, p. 11 defines variant discrimination rate as the fraction of mutations whose contracts do not verify, constrained by verification on the original. Surviving mutants tell the LLM what behavior its contract missed; it adds clauses that distinguish the original and returns to repair. The example, p. 12, strengthens missing return-value bounds. Algorithm 1 repeats until a 0.75 rejection threshold or iteration cap; §4.1, p. 13 sets repair and refinement caps to five.

§3.4 uses 188 C compiler-fuzzing mutation operators and GCC -O2 binary comparison to discard trivially equivalent programs. Exact quote: “consider them equivalent if the produced binary files are equal”. Inference: differing binaries do not prove differing source semantics. Trivial Compiler Equivalence filters some equivalent mutants, but cannot guarantee that all remaining mutants are behavior-changing. The operator count is not the number of mutants used per program.

The verifier returns unproved clauses, called “refuted” in Algorithm 1. Inference: failure to prove a mutant is not necessarily a concrete behavior violation; timeout, missing invariants or solver incompleteness can increase the measured rejection rate. Separate actual counterexamples, unknowns and budget failures before interpreting this score as semantic strength. Mutation also measures selected fault classes rather than all omitted guarantees.

Evidence

§§4.1–4.4, pp. 13–14 use GPT-4 Turbo, GPT-5 and DeepSeek-R1 with Frama-C/WP 25.0. The main dataset has 50 extracted self-contained files from 14 repository/task groups, with manually crafted reference ACSL contracts. Table 1 has group-average file sizes from 95 to 1,741 lines. This is larger-file evidence, not arbitrary whole-repository verification. Ground truth and the definition of reference coverage require care: §4.4 defines recall as “percentage of ground-truth specifications covered”, but does not detail a complete semantic coverage procedure in the main evaluation.

Table 1, p. 15 reports average precision/recall: GPT-5 96.68%/75.91%; GPT-4 94.52%/71.10%; DeepSeek-R1 95.80%/61.20%. Precision means “percentage of verifiable specifications over all generated specifications” (§4.4), not human-intent accuracy. Recall depends on the manually chosen reference set. These are author reports, not independent reproductions.

Table 2, p. 16 uses GPT-5. Without decomposition, precision/recall fall to 85.29%/63.25%; without refinement, 94.63%/70.57%. Arithmetic inference: decomposition loses 11.39 and 12.66 percentage points; the prose says 11.41 for precision. Refinement loses 2.05 and 5.34 points. The strongest measured benefit is decomposition; mutation adds a smaller increment while costing verifier calls.

Table 3, p. 17 has 1,365 supplied target assertions. SpecSyn proves 1,071: voronoi 153/172, Hypatia 187/195, sokol 220/241, X509-parser 132/142, Contiki 73/163, Atomthreads 130/239, and SV-COMP 132/220. The first three derive targets from docs/tests; the next three use runtime-error assertions from Preguss; the last category uses 220 small reachability programs averaging 27.79 lines. Preguss proves 503 total, AutoSpec 126, and the selected fine-tuned Llama model 29. Contiki is contrary evidence: Preguss proves 103 versus SpecSyn’s 73. The headline denominator therefore mixes large-file functional and safety properties with small reachability tasks.

§6, pp. 17–18 reports 3.62 hours per file versus Preguss’s 1.42 on the 50-file dataset, roughly 2.5× longer. Dollar costs, repeated-run uncertainty and runtime-by-mutation contribution are not provided in these results. A speedup through concurrent checking is suggested, not demonstrated.

Assurance, prior work and VL implications

The supplied target, all generated callee contracts, preconditions, memory model and solver outcome form the proof boundary. Recommendation: ensure generated callee contracts themselves are discharged and entry conditions are justified by callers; otherwise a target can pass under unsupported assumptions. Check precondition non-vacuity and permitted inputs separately. Recovering a property from buggy code can faithfully describe the bug, so ordinary docs/tests and stakeholder intent need an independent comparison.

§7, p. 18 identifies AutoSpec’s structural guidance, SpecGen’s repair, Preguss’s runtime-error analysis and prior mutation testing/compiler fuzzing. SpecSyn’s combination of dependency decomposition, explicit annotation sites, sketches and discrimination-driven refinement is already prior art. Existing specification notes already record its headline result and metric boundary; this study adds algorithm order, mutation-equivalence limitation, breakdown and ablations.

Recommendations for VL: segment Rust by dependencies; retain recursive groups; plan supporting contracts against fixed externally meaningful targets; generate one annotation site at a time; preserve verified clauses; use plausible behavior mutations to reveal omitted return bounds and relations; independently check verifier failure causes; assess mutation rejection on an unused mutation set; compare benefit with runtime expense. These are study recommendations only.

Product inference: supporting-contract recovery and mutation-strengthening directly overlap VL’s specification track. The native implementation is C/ACSL, so its empirical result does not establish Rust/Verus performance. But changing the language does not erase the prior algorithm. A useful VL distinction must be evidenced through repository-scale intent recovery, justified entry conditions and proof completion, rather than verifier-green or mutant rejection alone.

First reading: §§3.3–3.4 and §4.4. Ask whether a mutant’s failed verification means its behavior violates the contract or merely that the checker cannot finish the proof.

Study status

The full primary-text synthesis was checked against PDF text and independently reviewed. Local source links resolve. ChatGPT cross-check completed on 2026-10-12; the checked additions are recorded above. No implementation experiment was run.

ChatGPT cross-check (2026-10-12)

The complete ChatGPT answer was checked against specsyn.txt. These additions hold:

• the abstract reports SpecSyn “successfully handles 1071 out of 1365 target properties” (p. 1), but Table 3’s seven printed SpecSyn entries are 153, 187, 220, 132, 73, 130, and 132, which sum to 1,027, not 1,071 (§5.3, p. 17); the paper does not explain the discrepancy
• the paper defines the input as source code plus “verification targets (expressed as ACSL specifications)” (§3.1, p. 6), so the result is supporting-specification synthesis around supplied targets, not requirements-to-program synthesis
• the paper says binary files are considered equivalent when “the produced binary files are equal” (§3.4, p. 11); binary inequality therefore cannot by itself establish semantic non-equivalence
• the evaluation reports “approximately 2.5 times longer than Preguss” for SpecSyn’s per-file processing (§6, p. 18), so stronger specification generation comes with measured cost

The threat ratings and claims about verifier failures conflating semantic rejection with incompleteness are analysis. No artifact execution was performed.

Last edited: 2026-10-12