論文の概要: BTOR2-Based C Program Verification via Hardware Model Checking
- arxiv url: http://arxiv.org/abs/2607.17622v1
- Date: Mon, 20 Jul 2026 07:18:59 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-07-21 18:48:37.534572
- Title: BTOR2-Based C Program Verification via Hardware Model Checking
- Title（参考訳）: BTOR2によるハードウェアモデル検査によるCプログラムの検証
- Abstract要約: 本稿では,検証タスクをBTOR2モデルに符号化するC2Btorを提案する。
C2Btorは263のタスクを正しく解決する。
- 参考スコア（独自算出の注目度）: 10.596871975682978
- License: http://creativecommons.org/licenses/by-nc-nd/4.0/
- Abstract: Program verification tools often rely on specific intermediate representations and analysis backends, limiting the reuse of verification algorithms and model checkers across frameworks. In contrast, hardware model checking has developed a mature backend ecosystem, where standard formats such as BTOR2 support reusable algorithms for counterexample search and inductive safety proving. Applying these capabilities to C requires translating assertion-based programs into transition systems that hardware model checkers can directly process. We present C2Btor, a method for encoding such verification tasks into BTOR2 models. C2Btor uses a program counter to capture control transfers, represents data states and memory objects with bit-vectors and arrays, and maps assumptions and assertion checks into BTOR2 constraints and bad-state properties. We evaluate C2Btor on SV-COMP C ReachSafety benchmarks and a curated assertion-category benchmark suite, comparing it with representative program verification tools. C2Btor correctly solves 263 tasks, 101 more than CBMC configured with bounded model checking, and is especially effective on bit-vector benchmarks, where it solves 75.5% of the tasks with no wrong verdicts. These results show that the BTOR2 route allows C program verification to benefit from advances in hardware model-checking backends, expanding the available capability for counterexample search, inductive safety proving, and word-level transition-system reasoning.
- Abstract（参考訳）: プログラム検証ツールは、しばしば特定の中間表現と分析バックエンドに依存し、フレームワーク間の検証アルゴリズムとモデルチェッカーの再利用を制限する。
対照的に、ハードウェアモデルチェックは成熟したバックエンドエコシステムを構築しており、BTOR2のような標準フォーマットは、反例探索と帰納的安全性証明のための再利用可能なアルゴリズムをサポートする。
これらの機能をCに適用するには、ハードウェアモデルチェッカーが直接処理できる移行システムにアサーションベースのプログラムを変換する必要がある。
本稿では,このような検証タスクをBTOR2モデルに符号化するC2Btorを提案する。
C2Btorはプログラムカウンタを使用して制御転送をキャプチャし、ビットベクトルと配列でデータ状態とメモリオブジェクトを表現し、仮定とアサーションチェックをBTOR2制約とバッドステートプロパティにマップする。
SV-COMP C ReachSafetyベンチマークとアサーションカテゴリベンチマークスイート上でC2Btorを評価し,代表的なプログラム検証ツールと比較した。
C2Btorは263のタスクを正しく解決し、CBMCよりも101のタスクを境界モデルチェックに設定し、特にビットベクトルベンチマークで有効である。
これらの結果から,BTOR2経路は,ハードウェアモデルチェックバックエンドの進歩によるCプログラム検証の恩恵を享受し,反例探索,帰納的安全性証明,単語レベルのトランジッション・システム推論の能力の拡大を図っている。
関連論文リスト
- Agent-Driven Verification of Memory Safety for liblzma Decoder Components with VST [32.505127447635864]
Liblzmaのデコーダコンポーネントのメモリ安全性の検証について報告する。
検証の結果、生のLZMA1ゼロインプット処理における未定義の動作が明らかになった。
検証済みコードを合成する類似の作業とは異なり、既存のプロダクションスケールCを検証する。
論文 参考訳（メタデータ） (2026-08-30T10:50:56Z) - Circuit-Based Program Verification: Sequential Circuits as an Intermediate Representation for Verifying C Programs [5.82728420508304]
本稿では,ソフトウェア検証の中間表現としてシーケンシャル回路について検討する。
本稿では,Cプログラムを逐次回路に変換するモジュール型フレームワークであるCircuit-Based Program Verification(CPV)を提案する。
論文 参考訳（メタデータ） (2026-08-07T16:41:07Z) - KAT-Coder-V2.5 Technical Report [61.907486544595336]
KAT-Coder-V2.5は、実際の実行可能リポジトリ内で自律的に動作するよう訓練されたコーディング中心のエージェントモデルである。
マルチ言語リポジトリをサンドボックス環境に再構築し、フェイル・ツー・パスとパス・ツー・パスの検証を大規模に行う。
我々はさらに、ハーネスランダム化による強化学習、信頼性の強化されたサンドボックス、非対称なアクター-クリティックPPO、およびハイチ指向の報酬フレームワークをスケールする。
論文 参考訳（メタデータ） (2026-07-06T08:14:02Z) - PairCoder++: Pair Programming as a Universal Paradigm for Verified Code-Driven Multimodal and Structured-Artifact Generation [51.92442051257354]
PairCoderは、実行のみではなく、完全な公式メトリックスイート上で、アーティファクトが検証可能なすべてのベンチマークを本質的に改善する。
TikZのコンパイルレートは、各モデルで10から30ポイント、シングルモデルの2.9から9.2倍である。
論文 参考訳（メタデータ） (2026-07-02T08:36:02Z) - CIAware-Bench: Benchmarking Control Intervention Awareness Across Frontier LLMs [100.38986535324284]
我々は、フロンティアモデル全体でのtextbfcontrol textbfintervention (CI) の認識を測定するベンチマークである textbfCIAware-Bench を紹介する。
CIAware-Benchは、モデルが自身の軌跡を制御介入によって修正されたものと区別できるかどうかをテストする。
論文 参考訳（メタデータ） (2026-06-09T16:24:16Z) - LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation [75.05397479715576]
大規模言語モデル(LLM)とエージェントは有望な進歩を示しているが、その真の能力と失敗モードは未だ不明である。
CプログラムのためのLCMおよびエージェントベースの形式仕様生成に関する、最初の体系的および汚染に配慮した研究を提案する。
論文 参考訳（メタデータ） (2026-05-02T11:31:33Z) - WybeCoder: Verified Imperative Code Generation [22.401681809856896]
WybeCoderはエージェントコード検証フレームワークである。
コード、不変性、そして証明が共進化する所で、証明・アズ・ユー・ジェネレーション開発を可能にする。
論文 参考訳（メタデータ） (2026-03-31T00:06:44Z) - An Agentic Evaluation Framework for AI-Generated Scientific Code in PETSc [7.236134946837382]
petscagent-benchはエージェント評価エージェントのパラダイムに基づいて構築されたエージェントフレームワークである。
正確性、パフォーマンス、コード品質、アルゴリズムの適切性、ライブラリ固有の規約の5つの評価カテゴリで14評価パイプラインを編成する。
本フレームワークは,HPC用PETScライブラリを用いて,現実的な問題のベンチマークスイート上で実演する。
論文 参考訳（メタデータ） (2026-03-16T22:46:10Z) - ACE Runtime - A ZKP-Native Blockchain Runtime with Sub-Second Cryptographic Finality [1.7429038786735553]
既存の高性能ブロックチェーンは、クリティカルパス上のトランザクション毎にひとつのシグネチャを検証する。
本稿では、認証認証分離に基づくZKPネイティブ実行層であるACEについて述べる。
論文 参考訳（メタデータ） (2026-03-10T21:39:36Z) - Veri-Sure: A Contract-Aware Multi-Agent Framework with Temporal Tracing and Formal Verification for Correct RTL Code Generation [4.723302382132762]
シリコングレードの正しさは、 (i) シミュレーション中心の評価の限られたカバレッジと信頼性、 (ii) 回帰と修復幻覚、 (iii) エージェントハンドオフ間で意図が再解釈される意味的ドリフトによってボトルネックが残っている。
エージェントの意図を整合させる設計契約を確立するマルチエージェントフレームワークであるVeri-Sureを提案する。
論文 参考訳（メタデータ） (2026-01-27T16:10:23Z) - Every Step Counts: Decoding Trajectories as Authorship Fingerprints of dLLMs [63.82840470917859]
本稿では,dLLMの復号化機構をモデル属性の強力なツールとして利用できることを示す。
本稿では、デコードステップ間の構造的関係を捉え、モデル固有の振る舞いをよりよく明らかにする、DDM(Directed Decoding Map)と呼ばれる新しい情報抽出手法を提案する。
論文 参考訳（メタデータ） (2025-10-02T06:25:10Z) - SVTRv2: CTC Beats Encoder-Decoder Models in Scene Text Recognition [77.28814034644287]
テキストの不規則性や言語コンテキストのモデル化が可能なCTCモデルであるSVTRv2を提案する。
我々は,SVTRv2を標準ベンチマークと最近のベンチマークの両方で広範囲に評価した。
SVTRv2は精度と推論速度の点でほとんどのEDTRを超越している。
論文 参考訳（メタデータ） (2024-11-24T14:21:35Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。