AutoACSL: Synthesizing ACSL Specifications by Integrating LLMs with CPG-Based Static Analysis

• URL: http://arxiv.org/abs/2606.20969v1
• Date: Thu, 18 Jun 2026 22:16:23 GMT
• Title: AutoACSL: Synthesizing ACSL Specifications by Integrating LLMs with CPG-Based Static Analysis
• Abstract summary: We introduce AutoACSL, a framework that integrates large language models with semantic features extracted from Code Property Graphs (CPGs)<n>AutoACSL performs static analyses to extract key semantic elements, including arithmetic operations, loop and recursion structures, and return value propagation.<n>It achieves a 98% specification generation success ratio and a 96% full proof ratio when paired with Gemini-3.
• Score: 15.35068883163549
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Generating formal specifications for C programs remains a challenge in formal verification due to the manual effort, expertise, and semantic precision required. While recent advancements in large language models (LLMs) offer promise in automating specification synthesis, current approaches often lack semantic depth and produce unverifiable or incomplete contracts. To address these limitations, we introduce AutoACSL, a novel framework that integrates LLM prompting with semantic features extracted from Code Property Graphs (CPGs). AutoACSL performs static analyses to extract key semantic elements, including arithmetic operations, loop and recursion structures, and return value propagation, which are encoded into structured prompts. These prompts enable the LLM not only to generate normal behavioral specifications but also to include constraints that prevent inputs leading to runtime errors. AutoACSL employs a feedback-driven synthesis loop, where candidate specifications are verified using Frama-C/WP and refined iteratively until verification succeeds or a termination condition is met. Evaluated on 604 programs drawn from diverse datasets, AutoACSL achieves a 98% specification generation success ratio and a 96% full proof ratio when paired with Gemini-3. Compared to a code-only baseline, AutoACSL improves the full proof ratio by 24.7% to 51.7% across four LLMs (GPT-o4 Mini, GPT-5.2, Grok-4.1, and Gemini-3), demonstrating that integrating large language models with CPG-based static analysis substantially enhances both generation robustness and verification effectiveness for automated ACSL specification synthesis.

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)
• When LLMs Develop Languages: Symbolic Communication for Efficient Multi-Agent Reasoning [85.36421257648294]
  Chain-of-Thought (CoT) improves large language models (LLMs) on difficult reasoning tasks.<n>We propose Communicative Language Symbolism Routing (R)<n>R treats each Language Symbolism Framework as a reusable symbolic protocol with compact symbols, usage rules, and a message-passing contract.<n>R reduces latency-oriented generated token completion by $3sim 6times$ compared to standard CoT.
  arXiv  Detail & Related papers  (2026-06-28T12:02:42Z)
• Weave of Formal Thought [51.56484100374058]
  We introduce Weave of Formal Thought (WoFT), a paradigm uniting rigorous syntactic validation with learned structural representations.<n>We present a latent-variable fine-tuning method training the language model to interleave non-terminal grammar symbols directly into generation.<n>For Python, fine-tuning StarCoder2-3B with our RWS objective reduces per-token cross-entropy by 14.3% relative to a text-only SFT baseline.
  arXiv  Detail & Related papers  (2026-06-24T15:58:11Z)
• SpecSyn: LLM-based Synthesis and Refinement of Formal Specifications for Real-world Program Verification [10.586396714718457]
  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.
  arXiv  Detail & Related papers  (2026-04-23T11:46:19Z)
• Intent-aligned Formal Specification Synthesis via Traceable Refinement [43.72968325799861]
  We present VeriSpecGen, a traceable refinement framework that synthesizes intent-aligned specifications in Lean through requirement-level attribution and localized repair.<n>VeriSpecGen decomposes natural language into atomic requirements and generates requirement-targeted tests with explicit traceability maps.<n>We achieve 86.6% on VERINA SpecGen task using Claude Opus 4.5, improving over baselines by up to 31.8 points across different model families and scales.
  arXiv  Detail & Related papers  (2026-04-12T00:52:27Z)
• Evaluating LLM-Generated ACSL Annotations for Formal Verification [0.0]
  This paper empirically evaluates the extent to which formal-analysis tools can automatically generate and verify ACSL specifications without human or learning-based assistance.<n>Five ACSL generation systems are compared: a rule-based Python script, Frama-C's RTE plugin, and three large language models.<n>All generated specifications are verified under identical conditions using the Frama-C WP plugin powered by multiple SMT solvers.
  arXiv  Detail & Related papers  (2026-02-14T19:18:34Z)
• 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)
• From Memorization to Creativity: LLM as a Designer of Novel Neural-Architectures [48.83701310501069]
  Large language models (LLMs) excel in program synthesis, yet their ability to autonomously navigate neural architecture design-balancing reliability, performance, and structural novelty--remains underexplored.<n>We address this by placing a code-oriented LLM within a closed-loop synthesis framework, analyzing its evolution over 22 supervised fine-tuning cycles.
  arXiv  Detail & Related papers  (2026-01-06T13:20:28Z)
• 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)
• Federated Learning-Enabled Hybrid Language Models for Communication-Efficient Token Transmission [87.68447072141402]
  Hybrid Language Models (HLMs) combine the low-latency efficiency of Small Language Models (SLMs) on edge devices with the high accuracy of Large Language Models (LLMs) on centralized servers.<n>We propose FedHLM, a communication-efficient HLM framework that integrates uncertainty-aware inference with Federated Learning (FL)
  arXiv  Detail & Related papers  (2025-06-30T02:56:11Z)
• Towards Large Language Model Aided Program Refinement [10.089955747110444]
  Program refinement involves correctness-preserving transformations from formal high-level specification statements into executable programs. Large language models (LLMs) enable automatic code generations from informal natural language specifications. We propose LLM4PR, a tool that combines formal program refinement techniques with informal LLM-based methods.
  arXiv  Detail & Related papers  (2024-06-26T04:29:27Z)
• 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)
• Zero-Shot Cross-Lingual Summarization via Large Language Models [108.30673793281987]
  Cross-lingual summarization ( CLS) generates a summary in a different target language. Recent emergence of Large Language Models (LLMs) has attracted wide attention from the computational linguistics community. In this report, we empirically use various prompts to guide LLMs to perform zero-shot CLS from different paradigms.
  arXiv  Detail & Related papers  (2023-02-28T01:27:37Z)

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.