論文の概要: C*: Unifying Programming and Verification in C

• arxiv url: http://arxiv.org/abs/2504.02246v1
• Date: Thu, 03 Apr 2025 03:22:22 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-04-04 12:57:15.005363
• Title: C*: Unifying Programming and Verification in C
• Title（参考訳）: C*: 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要約: C* は C プログラミングのための言語設計の証明である。 プログラマが実装コードと並行して証明コードブロックを埋め込むことで、リアルタイムの検証を可能にする。 C* は C を共通言語として使用することで実装と証明コード開発を統合する。
• 参考スコア（独自算出の注目度）: 15.531046191957529
• License:
• 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.
• Abstract（参考訳）: システムソフトウェアの適切な機能を保証することは、その安全性に批判的かつ低レベルな性質を考えると、正式な検証研究と応用に重点を置いている。 検証ツールの進歩にもかかわらず、従来のプログラマは自身のコードの検証にほとんど関与せず、その結果、検証済みソフトウェアの開発とメンテナンスのコストが高くなる。 プログラマが検証プラクティスに参加する上で重要な障壁は、アクセシビリティとリアルタイムの検証を制限する、プログラミングと検証プラクティスの間の環境とパラダイムの切断である。 C*は、C言語プログラミングのための証明積分言語設計である。 C* は C を拡張して,シンボル実行エンジンと LCF スタイルの証明カーネルを使用した検証機能を備えている。 プログラマが実装コードと一緒に証明コードブロックを埋め込んで、現在の証明状態のインタラクティブな更新を容易にすることで、リアルタイムの検証を可能にする。 その表現力と拡張性のある証明サポートにより、ユーザーは論理的定義、定理、プログラム可能な証明自動化の再利用ライブラリを構築できる。 重要なことに、C*はC言語を共通言語として使用することによって実装と証明のコード開発を統合する。 我々は,C*のプロトタイプを実装し,小型Cプログラムの代表的ベンチマークで評価し,pKVMのアロケータのアタッチ関数である実世界のケーススタディに挑戦した。 以上の結果から,C*はCプログラミングイディオムの幅広いサブセットの検証をサポートし,実世界のシナリオにおける複雑な推論タスクを効果的に処理できることが示唆された。

関連論文リスト

• VisualCoder: Guiding Large Language Models in Code Execution with Fine-grained Multimodal Chain-of-Thought Reasoning [10.70881967278009]
  ビジュアル制御フローグラフ (CFG) を用いたマルチモーダルチェイン・オブ・ワットスニペット (CoT) 推論を統合することで,コード推論を強化する,シンプルかつ効果的なアプローチである VisualCoder を導入する。 我々は,参照機構によるマルチモーダルCoT統合の課題に対処し,コードと実行経路の整合性を確保し,プログラム動作予測,エラー検出,出力生成の性能を向上させる。
  論文  参考訳（メタデータ） (2024-10-30T19:07:01Z)
• Codev-Bench: How Do LLMs Understand Developer-Centric Code Completion? [60.84912551069379]
  Code-Development Benchmark (Codev-Bench)は、細粒度で現実世界、リポジトリレベル、開発者中心の評価フレームワークです。 Codev-Agentは、リポジトリのクローリングを自動化し、実行環境を構築し、既存のユニットテストから動的呼び出しチェーンを抽出し、データ漏洩を避けるために新しいテストサンプルを生成するエージェントベースのシステムである。
  論文  参考訳（メタデータ） (2024-10-02T09:11:10Z)
• Synthetic Programming Elicitation for Text-to-Code in Very Low-Resource Programming and Formal Languages [21.18996339478024]
  SPEAC(emphsynthetic programming elicitation and compilation)を紹介する。 SPEACは、より頻繁に、意味的正しさを犠牲にすることなく、構文的に正しいプログラムを生成する。 UCLID5形式検証言語のケーススタディにおいて,SPEACの性能を実証的に評価した。
  論文  参考訳（メタデータ） (2024-06-05T22:16:19Z)
• NExT: Teaching Large Language Models to Reason about Code Execution [50.93581376646064]
  大規模言語モデル(LLM)のコードは通常、プログラムの表面テキスト形式に基づいて訓練される。 NExTは,プログラムの実行トレースを検査し,実行時の動作を判断する手法である。
  論文  参考訳（メタデータ） (2024-04-23T01:46:32Z)
• Chain of Code: Reasoning with a Language Model-Augmented Code Emulator [115.16975276693267]
  我々は、LMコード駆動推論を改善するシンプルながら驚くほど効果的な拡張であるChain of Codeを提案する。 キーとなるアイデアは、プログラム内のセマンティックなサブタスクを、インタープリタが明示的にキャッチできるフレキシブルな擬似コードとしてフォーマットすることを、LMに促すことである。
  論文  参考訳（メタデータ） (2023-12-07T17:51:43Z)
• AdaCCD: Adaptive Semantic Contrasts Discovery Based Cross Lingual Adaptation for Code Clone Detection [69.79627042058048]
  AdaCCDは、その言語でアノテーションを使わずに、新しい言語のクローンコードを検出する新しい言語間適応手法である。 5つのプログラミング言語からなる多言語コードクローン検出ベンチマークを構築し,AdaCCDの言語間適応性を評価する。
  論文  参考訳（メタデータ） (2023-11-13T12:20:48Z)
• Klever: Verification Framework for Critical Industrial C Programs [0.0]
  我々は,大規模かつ重要な産業用Cプログラムに自動ソフトウェア検証ツールを適用する労力を削減するために,Kleverソフトウェア検証フレームワークを提案する。 既存のツールは、環境モデリング、要件の仕様、ターゲットプログラムの多くのバージョンと構成の検証、検証結果のエキスパートアセスメントなど、広く採用されている手段を提供していない。
  論文  参考訳（メタデータ） (2023-09-28T13:23:59Z)
• (Security) Assertions by Large Language Models [25.270188328436618]
  セキュリティのためのハードウェアアサーション生成において,コード生成に新たな大規模言語モデル(LLM)を用いることを検討する。 我々は、人気のあるLCMに注目し、プロンプトの様々なレベルの詳細を考慮し、アサーションを箱から書き出す能力を特徴付ける。
  論文  参考訳（メタデータ） (2023-06-24T17:44:36Z)
• Fact-Checking Complex Claims with Program-Guided Reasoning [99.7212240712869]
  Program-Guided Fact-Checking (ProgramFC)は、複雑なクレームを単純なサブタスクに分解する新しいファクトチェックモデルである。 まず,大規模言語モデルの文脈内学習能力を活用して推論プログラムを生成する。 我々は,各サブタスクを対応するサブタスクハンドラに委譲することでプログラムを実行する。
  論文  参考訳（メタデータ） (2023-05-22T06:11:15Z)
• CryptOpt: Verified Compilation with Randomized Program Search for Cryptographic Primitives (full version) [12.790826917588575]
  暗号は例外であり、多くのパフォーマンスクリティカルなルーチンがアセンブリで直接書かれてきた。 CryptOptは、GCCやClangが生成するものよりもはるかに高速なアセンブリコードに高レベルの暗号関数プログラムを専門とする、最初のコンパイルパイプラインである。 形式検証の面では、FiatOptフレームワーク(関数型プログラムをCライクなIRコードに変換する)に接続し、新たに公式に認証されたプログラム等価チェッカーで拡張する。
  論文  参考訳（メタデータ） (2022-11-19T11:07:39Z)
• Extending C++ for Heterogeneous Quantum-Classical Computing [56.782064931823015]
  qcorはC++とコンパイラの実装の言語拡張で、異種量子古典プログラミング、コンパイル、単一ソースコンテキストでの実行を可能にする。 我々の研究は、量子言語で高レベルな量子カーネル(関数)を表現できる、第一種C++コンパイラを提供する。
  論文  参考訳（メタデータ） (2020-10-08T12:49:07Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。