C*: Unifying Programming and Verification in C

• URL: http://arxiv.org/abs/2504.02246v1
• Date: Thu, 03 Apr 2025 03:22:22 GMT
• Title: C*: Unifying Programming and Verification in C
• Authors: Yiyuan Cao, Jiayi Zhuang, Houjin Chen, Jinkai Fan, Wenbo Xu, Zhiyi Wang, Di Wang, Qinxiang Cao, Yingfei Xiong, Haiyan Zhao, Zhenjiang Hu,
• Abstract summary: C* is a proof-integrated language design for C programming.<n>It enables real-time verification by allowing programmers to embed proof-code blocks alongside implementation code.<n>C* unifies implementation and proof code development by using C as the common language.
• Score: 15.531046191957529
• License: http://creativecommons.org/licenses/by-nc-nd/4.0/
• Abstract: Ensuring the correct functionality of systems software, given its safety-critical and low-level nature, is a primary focus in formal verification research and applications. Despite advances in verification tooling, conventional programmers are rarely involved in the verification of their own code, resulting in higher development and maintenance costs for verified software. A key barrier to programmer participation in verification practices is the disconnect of environments and paradigms between programming and verification practices, which limits accessibility and real-time verification. We introduce C*, a proof-integrated language design for C programming. C* extends C with verification capabilities, powered by a symbolic execution engine and an LCF-style proof kernel. It enables real-time verification by allowing programmers to embed proof-code blocks alongside implementation code, facilitating interactive updates to the current proof state. Its expressive and extensible proof support allows users to build reusable libraries of logical definitions, theorems, and programmable proof automation. Crucially, C* unifies implementation and proof code development by using C as the common language. We implemented a prototype of C* and evaluated it on a representative benchmark of small C programs and a challenging real-world case study: the attach function of pKVM's buddy allocator. Our results demonstrate that C* supports the verification of a broad subset of C programming idioms and effectively handles complex reasoning tasks in real-world scenarios.

Related papers

• Code to Think, Think to Code: A Survey on Code-Enhanced Reasoning and Reasoning-Driven Code Intelligence in LLMs [53.00384299879513]
  In large language models (LLMs), code and reasoning reinforce each other.<n>Code provides verifiable execution paths, enforces logical decomposition, and enables runtime validation.<n>We identify key challenges and propose future research directions to strengthen this synergy.
  arXiv  Detail & Related papers  (2025-02-26T18:55:42Z)
• VeCoGen: Automating Generation of Formally Verified C Code with Large Language Models [1.6249267147413524]
  VECOGEN is a novel tool that combines large language models with formal verification to automate the generation of formally verified C programs.<n>VECOGEN takes a formal specification in/ISO C Specification Language, a natural language specification, and a set of test cases to attempt to generate a verified program.
  arXiv  Detail & Related papers  (2024-11-28T17:12:21Z)
• VisualCoder: Guiding Large Language Models in Code Execution with Fine-grained Multimodal Chain-of-Thought Reasoning [10.70881967278009]
  We introduce VisualCoder, a simple yet effective approach that enhances code reasoning by integrating multimodal Chain-of-Thought snippets (CoT) reasoning with a visual Control Flow Graph (CFG)<n>We address challenges in multimodal CoT integration through a reference mechanism, ensuring consistency between code and its execution path, thereby improving performance in program behavior prediction, error detection, and output generation.
  arXiv  Detail & Related papers  (2024-10-30T19:07:01Z)
• Codev-Bench: How Do LLMs Understand Developer-Centric Code Completion? [60.84912551069379]
  We present the Code-Development Benchmark (Codev-Bench), a fine-grained, real-world, repository-level, and developer-centric evaluation framework. Codev-Agent is an agent-based system that automates repository crawling, constructs execution environments, extracts dynamic calling chains from existing unit tests, and generates new test samples to avoid data leakage.
  arXiv  Detail & Related papers  (2024-10-02T09:11:10Z)
• Synthetic Programming Elicitation for Text-to-Code in Very Low-Resource Programming and Formal Languages [21.18996339478024]
  We introduce emphsynthetic programming elicitation and compilation (SPEAC) SPEAC produces syntactically correct programs more frequently and without sacrificing semantic correctness. We empirically evaluate the performance of SPEAC in a case study for the UCLID5 formal verification language.
  arXiv  Detail & Related papers  (2024-06-05T22:16:19Z)
• NExT: Teaching Large Language Models to Reason about Code Execution [50.93581376646064]
  Large language models (LLMs) of code are typically trained on the surface textual form of programs. We propose NExT, a method to teach LLMs to inspect the execution traces of programs and reason about their run-time behavior.
  arXiv  Detail & Related papers  (2024-04-23T01:46:32Z)
• Chain of Code: Reasoning with a Language Model-Augmented Code Emulator [115.16975276693267]
  We propose Chain of Code, a simple yet surprisingly effective extension that improves LM code-driven reasoning. The key idea is to encourage LMs to format semantic sub-tasks in a program as flexible pseudocode that the interpreter can explicitly catch.
  arXiv  Detail & Related papers  (2023-12-07T17:51:43Z)
• AdaCCD: Adaptive Semantic Contrasts Discovery Based Cross Lingual Adaptation for Code Clone Detection [69.79627042058048]
  AdaCCD is a novel cross-lingual adaptation method that can detect cloned codes in a new language without annotations in that language. We evaluate the cross-lingual adaptation results of AdaCCD by constructing a multilingual code clone detection benchmark consisting of 5 programming languages.
  arXiv  Detail & Related papers  (2023-11-13T12:20:48Z)
• Klever: Verification Framework for Critical Industrial C Programs [0.0]
  We present the Klever software verification framework, designed to reduce the effort of applying automatic software verification tools to large and critical industrial C programs. Existing tools do not provide widely adopted means for environment modeling, specification of requirements, verification of many versions and configurations of target programs, and expert assessment of verification results.
  arXiv  Detail & Related papers  (2023-09-28T13:23:59Z)
• Fact-Checking Complex Claims with Program-Guided Reasoning [99.7212240712869]
  Program-Guided Fact-Checking (ProgramFC) is a novel fact-checking model that decomposes complex claims into simpler sub-tasks. We first leverage the in-context learning ability of large language models to generate reasoning programs. We execute the program by delegating each sub-task to the corresponding sub-task handler.
  arXiv  Detail & Related papers  (2023-05-22T06:11:15Z)
• CryptOpt: Verified Compilation with Randomized Program Search for Cryptographic Primitives (full version) [12.790826917588575]
  cryptography has been an exception, where many performance-critical routines have been written directly in assembly. We present CryptOpt, the first compilation pipeline that specializes high-level cryptographic functional programs into assembly code significantly faster than what GCC or Clang produce. On the formal-verification side, we connect to the FiatOpt framework (which translates functional programs into C-like IR code) and extend it with a new formally verified program-equivalence checker.
  arXiv  Detail & Related papers  (2022-11-19T11:07:39Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.