arXiv preprint ·
From Natural Language to Verified C: Verification-Guided Generation with ACSL Specifications
- Published
- Source
- arXiv preprint, posted before peer review
- Original
- Read it at arXiv
- Topics
Abstract
AI-assisted code generation amplifies the demand for automated formal verification. Generated programs must not only be executable but also accompanied by machine-checkable evidence of correctness. Existing approaches can synthesize functionally plausible code or plausible-looking specifications from natural-language prompts; however, they do not explicitly co-design the implementation and specification as a unified artifact optimized for verification. Consequently, automated verifiers often fail to discharge proof obligations. Typical failure modes include missing or implicit proof anchors, program structures that are hostile to automated reasoning, and inconsistencies between code-level state and specification-level requirement facts arising from the independent generation of code and specifications. Even when verification succeeds, it may only establish weak specifications that omit requirement-critical behavior. This paper introduces VeriGen-C, a formal-verification-friendly framework for the joint synthesis of C programs and ACSL specifications from natural-language requirements. Code generation and repair are constrained to expose proof-relevant state, to streamline control flow for deductive verification, and to eliminate implementation patterns that hinder automated proof search. Specification generation and refinement are similarly constrained to mitigate verification timeouts and to ensure alignment with the user requirements. Empirical evaluations on HumanEval-X, FM-Bench, and LiveCodeBench Lite demonstrate that VeriGen-C substantially improves the rate of verified and requirement-aligned solutions relative to an interface-compatible baseline, from 5.5% to 44.5%, from 44.3% to 80.0%, and from 6.5% to 58.7%, respectively.
The authors’ abstract, as arXiv lists it. arXiv’s listings, abstracts included, are free for anyone to reuse.
Read it on ReadSearch
Each opens after you create an account, and brings you back to this paper.
More in Software Engineering
Stale Instruction Files Override the Code in Coding Agents: A One-Sentence Fix
Are LLM-Generated Formal Specifications Faithful to Their Requirements? A Study on Bimodal Formal Specification Generation
Governance-State Corruption in Long-Term Memory for LLM Agents: A Cross-Model Stress Test
CrowdStrike Channel File 291: An Engineering Analysis of a Global Endpoint Outage
From Tokens to Credits to Outcomes: Pricing AI Across Models, Applications, and Cloud Platforms
Get the few papers worth your time in Software Engineering every morning.
ReadSearch reads the new papers in your field each day and brings you the few worth reading, each with its key finding in a sentence.