REVIEW 4 cited by
VeCoGen: Automating Generation of Formally Verified C Code with 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
Large language models have demonstrated impressive capabilities in generating code, yet they often produce programs with flaws or deviations from intended behavior, limiting their suitability for safety-critical applications. To address this limitation, this paper introduces VECOGEN, a novel tool that combines large language models with formal verification to automate the generation of formally verified C programs. VECOGEN takes a formal specification in ANSI/ISO C Specification Language, a natural language specification, and a set of test cases to attempt to generate a verified program. This program-generation process consists of two steps. First, VECOGEN generates an initial set of candidate programs. Secondly, the tool iteratively improves on previously generated candidates. If a candidate program meets the formal specification, then we are sure the program is correct. We evaluate VECOGEN on 15 problems presented in Codeforces competitions. On these problems, VECOGEN solves 13 problems. This work shows the potential of combining large language models with formal verification to automate program generation.
Forward citations
Cited by 4 Pith papers
-
GenOS: Compositional Certificates for Semantic Robustness in AI Code Generation
GenOS proves that equivalence-compatible Markov kernels in AI code generation pipelines compose, so equivalent prompts yield equal probabilities for observer-relative events like verified commit.
-
Natural-Language to SysMLv2 Translation via Conformance-Driven Iterative Refinement
Wrapping LLM generation in a loop that repairs until a production SysMLv2 checker reports zero errors lifts benchmark conformance from 51.16% single-shot to 100%, in at most 8 attempts per case.
-
Generating Automotive Code: Large Language Models for Software Development and Verification in Safety-Critical Systems
An LLM-based, feedback-driven code generation pipeline produced an ISO-inspired ACC implementation that passed static and CARLA simulation checks in all three test runs.
-
Survey of GenAI for Automotive Software Development: From Requirements to Executable Code
A review of roughly 60 papers and 9 industry respondents finds GPT-family models dominate automotive code generation while requirements handling lags due to confidentiality constraints.
Discussion (0). Continue with ORCID to comment.