VeCoGen: Automating Generation of Formally Verified C Code with Large Language Models
This program is tentative and subject to change.
Large Language Models (LLMs) 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 LLMs with formal verification to automate the generation of formally verified C programs. VeCoGen takes a formal specification in ANSI/ISO C Specification Language (ACSL), a natural language specification, and a set of test cases to attempt to generate a 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. VeCoGen is evaluated on 15 problems presented in Codeforces competitions. On these problems, VeCoGen solves 13 problems. This work shows the potential of combining LLMs with formal verification to automate program generation.
This program is tentative and subject to change.
Mon 28 AprDisplayed time zone: Eastern Time (US & Canada) change
11:00 - 12:30 | |||
11:00 30mTalk | LLM-based Generation of Weakest Preconditions and Precise Array Invariants Research Track | ||
11:30 30mTalk | VeCoGen: Automating Generation of Formally Verified C Code with Large Language Models Research Track Merlijn Sevenhuijsen Scania CV, AB & KTH Royal Institute of Technology, Khashayar Etemadi KTH Royal Institute of Technology, Mattias Nyberg Scania CV, AB & KTH Royal Institute of Technology | ||
12:00 30mTalk | Embracing Uncertainty: A Fuzzy Theoretical Model for Goal Fulfillment Assessment Research Track Vincenzo Grassi University of Roma "Tor Vergata", Raffaela Mirandola Karlsruhe Institute of Technology (KIT), Diego Perez-Palacin Linnaeus University |