SpecSyn: LLM-based Synthesis and Refinement of Formal Specifications for Real-world Program Verification

• URL: http://arxiv.org/abs/2604.21570v1
• Date: Thu, 23 Apr 2026 11:46:19 GMT
• Title: SpecSyn: LLM-based Synthesis and Refinement of Formal Specifications for Real-world Program Verification
• Abstract summary: SpecSyn is a novel LLM-based specification generation method.<n>In experiments, SpecSyn maintains high precision over 90% and outstanding recall over 75%.<n>In further evaluations, SpecSyn successfully handles 1071 out of 1365 target properties for open-source programs.
• Score: 10.586396714718457
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• 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.

Related papers

• ClarifyCodeBench: Evaluating LLMs on Clarifying Ambiguous Requirements for Code Generation [54.788849448970154]
  We introduce ClarifyCodeBench, a novel interactive benchmark for evaluating Large Language Models' capability in resolving requirement ambiguity.<n>We conduct a systematic evaluation of six state-of-the-art LLMs using ClarifyCodeBench.<n>Our empirical results yield three critical insights: 1) Capability Decoupling: Strong code generation performance does not inherently translate to effective requirement clarification; 2) The Reasoning Paradox: While increased computational thinking enhances code correctness, it yields marginal gains in identifying ambiguities.
  arXiv  Detail & Related papers  (2026-07-01T09:58:59Z)
• LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation [75.05397479715576]
  Large language models (LLMs) and agents have shown promising progress, but their true capabilities and failure modes remain unclear.<n>We present the first systematic and contamination-aware study of LLM- and agent-based formal specification generation for C programs.
  arXiv  Detail & Related papers  (2026-05-02T11:31:33Z)
• From Brute Force to Semantic Insight: Performance-Guided Data Transformation Design with LLMs [48.83701310501069]
  Large language models (LLMs) have achieved notable performance in code synthesis.<n>We introduce a performance-aware, closed-loop solution that enables LLMs to autonomously engineer optimal transformations.<n>We fine-tune LLMs with Low-Rank Adaptation on a novel repository of more than 6,000 empirically evaluated PyTorch augmentation functions.
  arXiv  Detail & Related papers  (2026-01-07T11:13:02Z)
• A Tale of 1001 LoC: Potential Runtime Error-Guided Specification Synthesis for Verifying Large-Scale Programs [34.387390697713556]
  This paper presents Preguss -- a modular, fine-grained framework for automating the generation and refinement of formal specifications.<n>We show that Preguss substantially outperforms state-of-the-art LLM-based approaches.<n>It enables highly automated RTE-freeness verification for real-world programs with over a thousand LoC, with a reduction of 80.6%88.9% human verification effort.
  arXiv  Detail & Related papers  (2025-12-31T03:31:51Z)
• Automated Constraint Specification for Job Scheduling by Regulating Generative Model with Domain-Specific Representation [38.193536141447254]
  This paper presents a constraint-centric architecture that regulates Large Language Models (LLMs) to perform reliable automated constraint specification for production scheduling.<n>An automated production scenario adaptation algorithm is designed and deployed to efficiently customize the architecture for specific manufacturing configurations. Experimental results demonstrate that the proposed approach successfully balances the generative capabilities of LLMs with the reliability requirements of manufacturing systems.
  arXiv  Detail & Related papers  (2025-10-03T02:34:11Z)
• SLD-Spec: Enhancement LLM-assisted Specification Generation for Complex Loop Functions via Program Slicing and Logical Deletion [29.231420590756954]
  SLD-Spec is an LLM-assisted specification generation method tailored for programs with complex loop constructs.<n>We show that SLD-Spec successfully verifies five more programs than the state-of-the-art AutoSpec and reduces runtime by 23.73%.
  arXiv  Detail & Related papers  (2025-09-12T01:40:27Z)
• Leveraging LLMs for Formal Software Requirements -- Challenges and Prospects [0.0]
  VERIFAI1 aims to investigate automated and semi-automated approaches to bridge this gap.<n>This position paper presents a preliminary synthesis of relevant literature to identify recurring challenges and prospective research directions.
  arXiv  Detail & Related papers  (2025-07-18T19:15:50Z)
• Specification-Guided Repair of Arithmetic Errors in Dafny Programs using LLMs [79.74676890436174]
  We present an APR tool for Dafny that uses formal specifications as oracles for fault localization and repair.<n>We localize faults through a series of steps, which include using Hoare logic to determine the state of each statement within the program.<n>Our tool achieves 89.6% fault localization coverage and GPT-4o mini yields the highest repair success rate of 74.18%.
  arXiv  Detail & Related papers  (2025-07-04T15:36:12Z)
• Training Language Models to Generate Quality Code with Program Analysis Feedback [66.0854002147103]
  Code generation with large language models (LLMs) is increasingly adopted in production but fails to ensure code quality.<n>We propose REAL, a reinforcement learning framework that incentivizes LLMs to generate production-quality code.
  arXiv  Detail & Related papers  (2025-05-28T17:57:47Z)
• Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification [15.686651364655958]
  AutoSpec is 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 can be successfully applied to verify the programs in a real-world X509-parser project.
  arXiv  Detail & Related papers  (2024-03-31T18:15:49Z)
• SpecGen: Automated Generation of Formal Program Specifications via Large Language Models [20.36964281778921]
  SpecGen is a novel technique for formal program specification generation based on Large Language Models.<n>We evaluate SpecGen on two datasets, including the SV-COMP 279 benchmark and a manually constructed dataset.
  arXiv  Detail & Related papers  (2024-01-16T20:13:50Z)
• Certified Reinforcement Learning with Logic Guidance [78.2286146954051]
  We propose a model-free RL algorithm that enables the use of Linear Temporal Logic (LTL) to formulate a goal for unknown continuous-state/action Markov Decision Processes (MDPs) The algorithm is guaranteed to synthesise a control policy whose traces satisfy the specification with maximal probability.
  arXiv  Detail & Related papers  (2019-02-02T20:09:32Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.