論文の概要: Circuit-Based Program Verification: Sequential Circuits as an Intermediate Representation for Verifying C Programs
- arxiv url: http://arxiv.org/abs/2608.07397v1
- Date: Fri, 07 Aug 2026 16:41:07 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-08-10 16:21:25.565601
- Title: Circuit-Based Program Verification: Sequential Circuits as an Intermediate Representation for Verifying C Programs
- Title（参考訳）: 回路に基づくプログラム検証:Cプログラムの中間表現としてのシーケンス回路
- Abstract要約: 本稿では,ソフトウェア検証の中間表現としてシーケンシャル回路について検討する。
本稿では,Cプログラムを逐次回路に変換するモジュール型フレームワークであるCircuit-Based Program Verification(CPV)を提案する。
- 参考スコア（独自算出の注目度）: 5.82728420508304
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Formal verification of software programs and hardware designs shares the common goal of reasoning about state-transition systems, yet the two communities have largely developed separate intermediate representations and verification algorithms. This paper investigates sequential circuits as an intermediate representation for software verification, with the goal of enabling direct application of hardware-model-checking techniques. We present Circuit-Based Program Verification (CPV), a modular framework that translates C programs into sequential circuits and employs off-the-shelf hardware model checkers as backends. Unlike traditional software verifiers, which typically rely on path-based exploration, CPV reasons over sequential circuits, where a program's control and data flows are folded into a monolithic transition relation that can be analyzed as a whole. The framework supports reachability-safety and termination analyses and integrates multiple state-of-the-art hardware model checkers, which together provide access to diverse verification algorithms, including bounded model checking, $k$-induction, and IC3/PDR. Counterexamples found by hardware model checkers are automatically translated back into software-verification witnesses for users to interpret verification results. We conducted a comprehensive evaluation on a benchmark suite of more than 16000 tasks. Our results show that CPV achieved competitive performance against five well-established software verifiers and exhibited complementary strengths by uniquely solving tasks that other verifiers cannot handle.
- Abstract（参考訳）: ソフトウェアプログラムとハードウェア設計の形式的検証は、状態遷移システムに関する推論という共通の目標を共有している。
本稿では,ハードウェア・モデル・チェック技術を直接適用することを目的とした,ソフトウェア検証の中間表現としてのシーケンシャル回路について検討する。
Cプログラムを逐次回路に変換し,既製のハードウェアモデルチェッカーをバックエンドとして使用するモジュール型フレームワークであるCircuit-Based Program Verification (CPV)を提案する。
通常パスベースの探索に依存する従来のソフトウェア検証装置とは異なり、CPVは、プログラムの制御とデータフローが全体として分析可能なモノリシックな遷移関係に折り畳まれるシーケンシャル回路よりも理由がある。
このフレームワークは、リーチビリティと終端分析をサポートし、複数の最先端ハードウェアモデルチェッカーを統合し、バウンドモデルチェック、$k$-induction、IC3/PDRを含む様々な検証アルゴリズムへのアクセスを提供する。
ハードウェアモデルチェッカーが見つけた反例は、ユーザーが検証結果を解釈するためのソフトウェア検証証人に自動的に変換される。
16000以上のタスクのベンチマークスイートに対して総合的な評価を行った。
以上の結果から,CPVは,確立された5つのソフトウェア検証に対して競争力を発揮し,他の検証者が扱えないタスクを一意に解くことで,補完的な強みを示した。
関連論文リスト
- Terminal Agents: A Survey of AI Agents in Command-Line Environments [102.48222742145474]
大規模言語モデルエージェントは、ターミナルを通してますます行動するが、既存の調査は、ソフトウェア工学、ツールの使用、コンピュータ利用の研究にまたがって端末による振る舞いを分散させている。
我々は,端末エージェントを,端末コマンドの実行,テキストフィードバック,ステートフルな環境相互作用を介し,進行を伴う動作を主とするシステムとみなす。
我々の合成は、実現された行動はモデル、インターフェース、ハーネス、ランタイム、環境によって共同で形成されていることを示している。
論文 参考訳（メタデータ） (2026-08-20T18:16:44Z) - Intent-Level Quantum Programming with Assertion-Guided Execution and Inspectable Intermediate Representation [0.22183164865527472]
量子ドメイン固有言語(Q)は3つのメカニズムを通して問題に対処する。
第1級IRイントロスペクション、回路幅の露光、ワイヤマッピング、操作順序、および実行前の開発者検査のための測定意図。
アサーション誘導モード推論では、エンジンが宣言された検証プロパティを調べて、サンプリング、ステートベクタ、デュアル実行を自動的に選択する。
論文 参考訳（メタデータ） (2026-07-31T18:21:32Z) - BTOR2-Based C Program Verification via Hardware Model Checking [10.596871975682978]
本稿では,検証タスクをBTOR2モデルに符号化するC2Btorを提案する。
C2Btorは263のタスクを正しく解決する。
論文 参考訳（メタデータ） (2026-07-20T07:18:59Z) - EquivFusion: Unifying Hardware Equivalence Checking from Algorithms to Netlists via MLIR [14.681439854488765]
EquivFusionはマルチモーダル回路の設計に適したエンドツーエンドの等価チェックツールである。
PyTorch、C/C++、Chisel、Verilog、ゲートレベルのネットリストなど、さまざまなエントリポイントを共通の中間表現に統合する。
論文 参考訳（メタデータ） (2026-04-17T12:09:54Z) - UniDial-EvalKit: A Unified Toolkit for Evaluating Multi-Faceted Conversational Abilities [70.79422099851506]
対話型AIシステム評価のための統合評価ツールキットUniDial-EvalKit(UDE)を提案する。
UDEは異種データフォーマットを普遍的なスキーマに標準化し、モジュールアーキテクチャを通じて複雑な評価パイプラインを合理化し、一貫したスコアリングインターフェースの下でメートル法計算を調整する。
論文 参考訳（メタデータ） (2026-03-24T13:01:31Z) - Scaling Agentic Verifier for Competitive Coding [66.11758166379092]
大規模言語モデル(LLM)は強力なコーディング能力を示しているが、1回の試行で競合するプログラミング問題を正しく解くのに苦戦している。
実行ベースの再ランク付けは、有望なテスト時間スケーリング戦略を提供するが、既存のメソッドは、難しいテストケースの生成または非効率的なランダム入力サンプリングによって制約される。
本稿では,プログラムの動作を積極的に推論し,高い差別性のあるテスト入力を検索するエージェント検証手法を提案する。
論文 参考訳（メタデータ） (2026-02-04T06:30:40Z) - 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) - A General Framework for Verification and Control of Dynamical Models via Certificate Synthesis [54.959571890098786]
システム仕様を符号化し、対応する証明書を定義するためのフレームワークを提供する。
コントローラと証明書を形式的に合成する自動化手法を提案する。
我々のアプローチは、ニューラルネットワークの柔軟性を利用して、制御のための安全な学習の幅広い分野に寄与する。
論文 参考訳（メタデータ） (2023-09-12T09:37:26Z) - Adaptive Planning Search Algorithm for Analog Circuit Verification [53.97809573610992]
シミュレーションの少ない機械学習(ML)アプローチを提案する。
提案手法により,OCCを全回路の仕様に近づけることができることを示す。
論文 参考訳（メタデータ） (2023-06-23T12:57:46Z) - CoCoMoT: Conformance Checking of Multi-Perspective Processes via SMT
(Extended Version) [62.96267257163426]
我々はCoCoMoT(Computing Conformance Modulo Theories)フレームワークを紹介する。
まず、純粋な制御フロー設定で研究したSATベースのエンコーディングを、データ認識ケースに持ち上げる方法を示す。
次に,プロパティ保存型クラスタリングの概念に基づく新しい前処理手法を提案する。
論文 参考訳（メタデータ） (2021-03-18T20:22:50Z) - Controlled time series generation for automotive software-in-the-loop
testing using GANs [0.5352699766206808]
オートマチックメカトロニクスシステムのテストは、部分的にはソフトウェア・イン・ザ・ループ・アプローチを使用し、システム・アンダー・テストのインプットを体系的にカバーすることが大きな課題である。
ひとつのアプローチは、テストプロセスの制御とフィードバックを容易にする入力シーケンスを作成することだが、現実的なシナリオにシステムを公開できない。
もうひとつは、現実を説明できるフィールド操作から記録されたシーケンスを再生するが、広く使われるには十分なキャパシティの十分なラベル付きデータセットを収集する必要があるため、コストがかかる。
この研究は、GAN(Generative Adrial Networks)のよく知られた教師なし学習フレームワークを適用して、記録された車内データのラベルなしデータセットを学習する。
論文 参考訳（メタデータ） (2020-02-16T16:19:29Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。