REVIEW 9 cited by
SpecGen: Automated Generation of Formal Program Specifications via Large Language Models
Not yet reviewed by Pith; the record is open.
This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.
SPECIMEN: schema-true, not a live event
T0 review · schema-true
One-sentence machine reading of the paper's core claim.
pith:XXXXXXXX · record.json · timestamp
read the original abstract
Formal program specifications play a crucial role in various stages of software development. However, manually crafting formal program specifications is rather difficult, making the job time-consuming and labor-intensive. It is even more challenging to write specifications that correctly and comprehensively describe the semantics of complex programs. To reduce the burden on software developers, automated specification generation methods have emerged. However, existing methods usually rely on predefined templates or grammar, making them struggle to accurately describe the behavior and functionality of complex real-world programs. To tackle this challenge, we introduce SpecGen, a novel technique for formal program specification generation based on Large Language Models. Our key insight is to overcome the limitations of existing methods by leveraging the code comprehension capability of LLMs. The process of SpecGen consists of two phases. The first phase employs a conversational approach that guides the LLM to generate appropriate specifications for a given program. The second phase, designed for where the LLM fails to generate correct specifications, applies four mutation operators to the model-generated specifications and selects verifiable specifications from the mutated ones through a novel heuristic selection strategy. We evaluate SpecGen on two datasets, including the SV-COMP Java category benchmark and a manually constructed dataset. Experimental results demonstrate that SpecGen succeeds in generating verifiable specifications for 279 out of 385 programs, outperforming the existing purely LLM-based approaches and conventional specification generation tools like Houdini and Daikon. Further investigations on the quality of generated specifications indicate that SpecGen can comprehensively articulate the behaviors of the input program.
Forward citations
Cited by 9 Pith papers
-
VeriSkill: A Self-Evolution Framework for Program Verification Skills
VeriSkill turns failed program-verification attempts into validated, reusable skill updates, reporting PASS-rate gains of 17.6 to 51.3 percentage points over no-skill agents across Dafny, Frama-C, and VeriFast.
-
Breaking the Myth: Can Small Models Infer Postconditions Too?
Fine-tuning Qwen2.5-Coder-7B on 1.5K reasoning examples yields postcondition generation close to GPT-4o and better than 32B open models on Defects4J.
-
gigiProfiler: Diagnosing Performance Issues by Uncovering Application Resource Bottlenecks
gigiProfiler combines an LLM resource spotter with static validation to find application-level bottlenecks and root-cause variables by comparing buggy and normal executions.
-
Supporting Software Formal Verification with Large Language Models: An Experimental Study
Automated LLM-to-ESBMC requirements verification on Lockheed Martin benchmarks reaches a 46.5% verification rate, matching NASA's CoCoSim with fewer false positives.
-
Requirements Development and Formalization for Reliable Code Generation: A Multi-Agent Vision
The paper proposes ReDeFo, a multi-agent pipeline that uses formal specifications and verification to generate reliable code from natural language requirements.
-
Leveraging LLMs for Formal Software Requirements -- Challenges and Prospects
LLM-based formalisation of software requirements is promising but faces five persistent challenges; the proposed VERIFAI framework plans to address them with human-in-the-loop and tool-neutral pipelines.
-
LLM-Based Agentic Systems for Software Engineering: Challenges and Opportunities
A survey of LLM-based multi-agent systems across the software development life cycle, plus a research agenda for orchestration, human coordination, cost, and data.
-
A Short Survey on Formalising Software Requirements using Large Language Models
A survey summarizing 35 papers on using LLMs to formalize software requirements, but it contains no new experimental results and its classification tables have errors.
-
Formalising Software Requirements using Large Language Models
A short project-position paper describing VERIFAI, a planned system for automatic formalisation and traceability of natural language requirements, with no experimental results yet.
Discussion (0). Sign in to comment.