Cover Image

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

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Ma, Lezhi, Liu, Shangqing, Li, Yi, Wu, Qiong, Wang, Han, Bu, Lei
Format:	Preprint
Published:	2026
Subjects:	Software Engineering
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

SpecGen: Automated Generation of Formal Program Specifications via Large Language Models
by: Ma, Lezhi, et al.
Published: (2024)

SpecEval: Evaluating Code Comprehension in Large Language Models via Program Specifications
by: Ma, Lezhi, et al.
Published: (2024)

Intention is All You Need: Refining Your Code from Your Intention
by: Guo, Qi, et al.
Published: (2025)

Structural Abstraction and Selective Refinement for Formal Verification
by: Luckeneder, Christoph, et al.
Published: (2025)

FormalSpecCpp: A Dataset of C++ Formal Specifications created using LLMs
by: Chakraborty, Madhurima, et al.
Published: (2025)

Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification
by: Wen, Cheng, et al.
Published: (2024)

Doc2Spec: Synthesizing Formal Programming Specifications from Natural Language via Grammar Induction
by: Xia, Shihao, et al.
Published: (2026)

Combining Fine-Tuning and LLM-based Agents for Intuitive Smart Contract Auditing with Justifications
by: Ma, Wei, et al.
Published: (2024)

Combining LLM Code Generation with Formal Specifications and Reactive Program Synthesis
by: Murphy, William, et al.
Published: (2024)

EPSO: A Caching-Based Efficient Superoptimizer for BPF Bytecode
by: Zhu, Qian, et al.
Published: (2025)

Automatic Generation of Formal Specification and Verification Annotations Using LLMs and Test Oracles
by: Faria, João Pascoal, et al.
Published: (2026)

Towards an Agentic LLM-based Approach to Requirement Formalization from Unstructured Specifications
by: Tagliaferro, Alberto, et al.
Published: (2026)

PropertyGPT: LLM-driven Formal Verification of Smart Contracts through Retrieval-Augmented Property Generation
by: Liu, Ye, et al.
Published: (2024)

Enhancing LLM-based Specification Generation via Program Slicing and Logical Deletion
by: Chen, Zehan, et al.
Published: (2025)

Reinforcement Learning with Negative Tests as Completeness Signal for Formal Specification Synthesis
by: Huang, Zhechong, et al.
Published: (2026)

CodeGrad: Integrating Multi-Step Verification with Gradient-Based LLM Refinement
by: Zhang, Yueke, et al.
Published: (2025)

What Makes a Good LLM Agent for Real-world Penetration Testing?
by: Deng, Gelei, et al.
Published: (2026)

VeriAct: Beyond Verifiability -- Agentic Synthesis of Correct and Complete Formal Specifications
by: Misu, Md Rakib Hossain, et al.
Published: (2026)

DafnyPro: LLM-Assisted Automated Verification for Dafny Programs
by: Banerjee, Debangshu, et al.
Published: (2026)

Formal Verification of Legal Contracts: A Translation-based Approach (Extended Version)
by: Hähnle, Reiner, et al.
Published: (2025)

DiffSpec: Differential Testing with LLMs using Natural Language Specifications and Code Artifacts
by: Rao, Nikitha, et al.
Published: (2024)

AutoSpec: Automated Generation of Neural Network Specifications
by: Jin, Shuowei, et al.
Published: (2024)

Formal Verification of Consistency for Systems with Redundant Controllers
by: Johansson, Bjarne, et al.
Published: (2024)

CodeSpecBench: Benchmarking LLMs for Executable Behavioral Specification Generation
by: Chen, Zaoyu, et al.
Published: (2026)

Integrating Various Software Artifacts for Better LLM-based Bug Localization and Program Repair
by: Feng, Qiong, et al.
Published: (2024)

Incorporating Verification Standards for Security Requirements Generation from Functional Specifications
by: Lian, Xiaoli, et al.
Published: (2025)

An Agile Formal Specification Language Design Based on K Framework
by: Zhang, Jianyu, et al.
Published: (2024)

FLAG: Formal and LLM-assisted SVA Generation for Formal Specifications of On-Chip Communication Protocols
by: Shih, Yu-An, et al.
Published: (2025)

FT2Ra: A Fine-Tuning-Inspired Approach to Retrieval-Augmented Code Completion
by: Guo, Qi, et al.
Published: (2024)

SpecTra: Enhancing the Code Translation Ability of Language Models by Generating Multi-Modal Specifications
by: Nitin, Vikram, et al.
Published: (2024)

A Hypergraph-based Formalization of Hierarchical Reactive Modules and a Compositional Verification Method
by: Ishii, Daisuke
Published: (2024)

ContrastRepair: Enhancing Conversation-Based Automated Program Repair via Contrastive Test Case Pairs
by: Kong, Jiaolong, et al.
Published: (2024)

ProofWright: Towards Agentic Formal Verification of CUDA
by: Chatterjee, Bodhisatwa, et al.
Published: (2025)

ReSyn: A Generalized Recursive Regular Expression Synthesis Framework
by: Kim, Seongmin, et al.
Published: (2026)

Lemma Discovery in Agentic Program Verification
by: Zhao, Huan, et al.
Published: (2026)

Beyond Basic Specifications? A Systematic Study of Logical Constructs in LLM-based Specification Generation
by: Chen, Zehan, et al.
Published: (2026)

Intent-aligned Formal Specification Synthesis via Traceable Refinement
by: Ye, Zhe, et al.
Published: (2026)

Event-B Agent: Towards LLM Agent for Formal Model Synthesis and Repair
by: Wang, Hongshu, et al.
Published: (2026)

A Survey on LLM-based Code Generation for Low-Resource and Domain-Specific Programming Languages
by: Joel, Sathvik, et al.
Published: (2024)

Can Large Language Models Model Programs Formally?
by: Chen, Zhiyong, et al.
Published: (2026)