Agentic Separation Logic Specification Synthesis

• URL: http://arxiv.org/abs/2605.27531v1
• Date: Tue, 26 May 2026 18:05:42 GMT
• Title: Agentic Separation Logic Specification Synthesis
• Abstract summary: Spec-Agent is an agentic system for synthesizing expressive, well-validated specifications across large C++s.<n>For each function, Spec-Agent uses static analysis and runtime heap tracing to select the appropriate target specification language.<n>We evaluate Spec-Agent on open source C++s comprising millions of lines of code.
• Score: 4.177196802192322
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Specification synthesis, the task of automatically inferring formal specifications from program implementations and natural language, is important for refactoring, transpilation, optimization, and verification, yet remains an open challenge for large C++ repositories. Existing LLM-based approaches fail to simultaneously scale to such repositories, produce specifications expressive enough to capture systems-code features such as dynamic memory and heap-allocated data structures, and systematically validate those specifications to rule out incorrect candidates. We present Spec-Agent, an agentic system for synthesizing expressive, well-validated specifications across large C++ codebases. Spec-Agent targets a ladder of specification languages: propositional logic, first-order logic, propositional separation logic, and first-order separation logic. For each function, Spec-Agent uses static analysis and runtime heap tracing to select the appropriate target specification language, generalizes existing functional tests into fuzz harnesses, and iteratively refines LLM-generated candidates via counterexample-guided feedback. We evaluate Spec-Agent on open source C++ codebases comprising millions of lines of code. Spec-Agent synthesizes valid specifications for 85% of target functions, with no false positives observed under fuzzing and expert validation, outperforming Claude Code Opus 4.6 at 10x lower token cost.

Related papers

• The Imitation Game: When LLMs Learn to Reason Like Programs via Code-Centric Reasoning Data Synthesis [50.473217152006875]
  MIMIC is a framework that leverages executable code as a rigorous medium for reasoning data synthesis.<n>MIMIC transforms algorithms into verifiable reasoning trajectories through narrative fusion, code-guided test synthesis, and dynamic code instrumentation.<n>Our method significantly elevates accuracy across general reasoning, complex mathematical benchmarks, and fine-grained deterministic tasks.
  arXiv  Detail & Related papers  (2026-09-13T17:04:16Z)
• Formal Verification of Agentic Systems over Operational Data [59.98246281888422]
  Agentic systems driven by large language models (LLMs) are increasingly deployed in real-world where they act on persistent operational data.<n>Existing approaches do not provide such system-level guarantees.<n>We study here the verification of agentic systems comprising a single LLM and a tool orchestration harness over relational operational data.
  arXiv  Detail & Related papers  (2026-08-04T13:01:30Z)
• RepoReasoner: Evaluating Repository-Level Code Reasoning Ability of Long-Context Language Models [54.53236295237077]
  We introduce RepoReasoner, a benchmark for evaluating repository-level code reasoning.<n> Output Prediction measures fine-grained, stateful execution reasoning across files.<n>Call Chain Prediction evaluates high-level architectural dependency understanding under noisy context.
  arXiv  Detail & Related papers  (2026-07-28T17:12:41Z)
• 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)
• LLM-Based Static Verification of Code Against Natural-Language Requirements: An Industrial Experience Report [3.5867640049033054]
  This article presents a two-stage LLM-based workflow for addressing this challenge in an intelligent-vehicle cybersecurity case study.<n>In the first stage, an AI-based rule miner extracts verifiable rules from natural-language requirements.<n>In the second stage, an AI-based code auditor checks implementation evidence against the extracted rules.
  arXiv  Detail & Related papers  (2026-05-18T06:34:03Z)
• From I/O to Code with Discovery Agent [103.88427301265669]
  We propose DIO-Agent, a discovery agent for IO2Code.<n>Our method frames IO2Code as an evolutionary search over discrete program space.<n>Extensive experiments show that DIO-Agent consistently outperforms both traditional program-by-example method and SOTA evolution-agent baselines.
  arXiv  Detail & Related papers  (2026-05-14T18:57:32Z)
• Neuro-Symbolic Generation and Validation of Memory-Aware Formal Function Specifications [12.783777562919383]
  Formal verification of memory-manipulating programs critically depends on precise function specifications that capture memory states written by experts.<n>We propose a neuro-symbolic framework for automatically generating memory-aware formal function specifications for C programs.<n>We introduce LeetCode-C-Spec, a new benchmark of 200 C programming problems for generating memory-aware formal function specifications.
  arXiv  Detail & Related papers  (2026-03-12T15:02:26Z)
• Understanding by Reconstruction: Reversing the Software Development Process for LLM Pretraining [66.89012795621349]
  Large Language Models (LLMs) often struggle with the deep, long-horizon reasoning required for complex software engineering.<n>We propose a novel paradigm: understanding via reconstruction.<n>We introduce a framework that synthesizes latent agentic trajectories using a multi-agent simulation.
  arXiv  Detail & Related papers  (2026-03-11T09:23:20Z)
• SpecMap: Hierarchical LLM Agent for Datasheet-to-Code Traceability Link Recovery in Systems Engineering [8.235446273226277]
  Traceability between embedded systemss and their corresponding code implementations is a fundamental challenge in systems engineering.<n>Existing Traceability Link Recovery approaches rely on lexical similarity and information retrieval techniques.<n>We present a hierarchical-to-code mapping methodology that employs large language models for semantic analysis.
  arXiv  Detail & Related papers  (2026-01-16T11:50:18Z)
• Connecting the Dots: Training-Free Visual Grounding via Agentic Reasoning [63.109585527799005]
  GroundingAgent is a visual grounding framework that operates without task-specific fine-tuning.<n>It achieves an average zero-shot grounding accuracy of 65.1 % on widely-used benchmarks.<n>It also offers strong interpretability, transparently illustrating each reasoning step.
  arXiv  Detail & Related papers  (2025-11-24T03:11:08Z)
• 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)
• AGENTIF: Benchmarking Instruction Following of Large Language Models in Agentic Scenarios [51.46347732659174]
  Large Language Models (LLMs) have demonstrated advanced capabilities in real-world agentic applications.<n>AgentIF is the first benchmark for systematically evaluating LLM instruction following ability in agentic scenarios.
  arXiv  Detail & Related papers  (2025-05-22T17:31:10Z)
• 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)

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.