論文の概要: Function Contracts for Bounded Model Checking of C Programs

• arxiv url: http://arxiv.org/abs/2610.26089v1
• Date: Mon, 19 Oct 2026 09:51:05 GMT
• ステータス: 情報取得中
• システム内更新日: 2026-10-21 06:56:28.355797
• Title: Function Contracts for Bounded Model Checking of C Programs
• Title（参考訳）: Cプログラムの境界モデルチェックのための関数契約
• Abstract要約: 本稿ではESBMCの関数抽出フレームワークについて述べる。 節の構文、両方のフェーズ、ツールが行った最初の実行方法がここで紹介されている。
• 参考スコア（独自算出の注目度）: 10.739711394746339
• License:
• Abstract: Bounded model checking unrolls a program into a single formula, so a function holding a loop costs the solver a fresh copy of that loop at every call site. Function contracts break that coupling. Verify the body once against its contract, then replace each call by a stub derived from it. CBMC supports this through dynamic frame condition checking, applied at industrial scale, but with no formal account of why the replacement is sound and no characterisation of what the frame check costs. We present the function-contract framework for ESBMC. The clause syntax, both phases, and the first assigns enforcement the tool has had are all introduced here. Its technical core is an observational frame rule: snapshot the locations the contract does not permit the function to write, then compare them at exit. The encoding emits a number of verification conditions set by how many globals the program has, not by how many writes the body performs, while dynamic frame condition checking grows with the write count. That is a property of the encoding rather than a timing, so it moves with neither the machine nor the solver. The rule itself is the classical one; what we add is its bounded form inside a BMC encoding, with the pipeline's algebraic skeleton machine-checked in Lean 4 and the limits of that model stated. We evaluate on synthetic sweeps, SV-COMP tasks, an ANSSI X.509 parser, the FreeRTOS heap_1 allocator, and the ML-KEM reference implementation whose CBMC contracts we reuse unchanged. At the coefficient count FIPS-203 mandates, neither tool finishes on the monolithic route inside ten minutes, and both finish on the modular one. The framework is merged into ESBMC master. Contracts are what is left when unrolling runs out of room.
• Abstract（参考訳）: 境界モデルチェックはプログラムを1つの公式にアンロールするので、ループを保持する関数は、各呼び出しサイトでそのループを新たにコピーする。 機能契約はその結合を壊します。 一度その体をその契約に反して検証し、それからそれぞれの呼び出しをそこから派生したスタブで置き換える。 CBMCは、産業規模で適用された動的フレーム条件チェックを通じてこれをサポートしているが、なぜ交換が健全であるかという公式な説明はなく、フレームチェックのコストの特徴も示していない。 本稿ではESBMCの関数抽出フレームワークについて述べる。 節の構文、両方のフェーズ、そしてツールが行っていた強制を最初に割り当てる。 コントラクトが関数の記述を許可しない位置をスナップショットし、終了時にそれらを比較します。 エンコーディングは、プログラムのグローバルな数によって設定された多数の検証条件を出力し、ボディの書き込み数ではなく、動的フレーム条件チェックは書き込み数とともに増加する。 これはタイミングではなく符号化の特性なので、マシンもソルバも動かない。 私たちが加えるのは、パイプラインの代数的スケルトンをLean 4でマシンでチェックし、そのモデルの限界を記述した、BMCエンコーディング内のバウンド形式です。 我々は, 合成スイープ, SV-COMPタスク, ANSSI X.509パーサ, FreeRTOS heap_1アロケータ, CBMC契約を再利用しないML-KEM参照実装について検討した。 係数数 FIPS-203 では、どちらのツールも10分以内にモノリシックルートで終了し、どちらもモジュラールートで終了する。 フレームワークはESBMCマスタにマージされます。 部屋がなくなると、契約が残ります。

関連論文リスト

• Resume Means Resume: A Machine-Checked Conformance Contract for Checkpoint, Interrupt, and Resume Semantics in Workflow Persistence Layers [0.0]
  実行状態を維持して、実行を中断し、クラッシュを生き残るためのフレームワークは、すでに発生した影響に対して、再開が何を意味するのかを判断し続けなければなりません。 5つの広くデプロイされたエージェントワークフローフレームワークがそれぞれ異なる答えを出し、マシンチェック可能なコントラクトを公開することはない。 LangGraph 1.2.9は2度目の履歴書値を記録し、それを参照せず、無意味な状態を静かに持続し、実際のSIGKILLの後、永続的に記録された作業を再実行する。
  論文  参考訳（メタデータ） (2026-08-04T15:45:31Z)
• Concurrent Image Understanding and Generation: Self-Correcting Coupled Markov Jump Processes [70.61868608402723]
  我々は$textbfSelf-Correcting Coupled Markov Jump Processes (SC-CMJP)を紹介する。 SC-CMJPと組み合わせて、共同マルチモーダルジェネレーションのための新しいトレーニングフリーシングルパスサンプリングであるtextttCO_texttt2textttJump$を紹介する。 トレーニングと評価のために,我々は3つの大規模ジョイントマルチモーダル生成コーパスを作成し,リリースする。
  論文  参考訳（メタデータ） (2026-07-14T18:39:29Z)
• Function-Aware Fill-in-the-Middle as Mid-Training for Coding Agent Foundation Models [49.259951930558]
  コーディングエージェントは、継続的な推論に外部ツールリターンを統合する必要がある。 我々は,中等教育における機能意識の充足を通じてこれを活用する。
  論文  参考訳（メタデータ） (2026-07-14T07:44:26Z)
• Partial Contracts Suffice: Sound, LLM-Inferred Regression Verification [7.004725450780227]
  本稿では,契約に基づく回帰検証ツールについて紹介する。 契約の健全性は、すべての関数バージョンが振舞いと一致することを証明することによって保証される。 完全な振る舞い仕様ではなく、部分的かつ呼び出し側対応の契約で十分かどうかを問う。
  論文  参考訳（メタデータ） (2026-07-11T12:40:22Z)
• SCDBench: A Benchmark for LLM-Based Smart Contract Decompilers [55.39407031861402]
  本稿では,スマートコントラクトデコンパイルのためのデータセットとベンチマーク手法であるSCDBenchを紹介する。 データセットには600の現実のSolidityコントラクトと、ペア化されたバイトコード入力、地味なソースコード、再生可能なセマンティックチェックポイントが含まれている。 我々は,GLM-5の変種を含むゼロショット逆コンパイル設定において,Claude Opus 4.7,GPT-5.3-Codex,GLM-5を評価した。
  論文  参考訳（メタデータ） (2026-05-27T20:08:47Z)
• LACUNA: Safe Agents as Recursive Program Holes [3.2613419151327343]
  LLMエージェントはますますコードを記述することで振る舞うが、エージェントを駆動するランタイムとモデルが記述するコードの間には分割が持続する。 我々は、安全性を維持しながら、この分割を閉じるエージェントのためのプログラミングモデルであるLACUNAを紹介する。 我々のプリミティブは、通常の制御フローとしてReActループ、サブエージェント、スキル、並列分解、マルチモデル計画を表現する。
  論文  参考訳（メタデータ） (2026-05-27T15:27:25Z)
• SolBench: A Dataset and Benchmark for Evaluating Functional Correctness in Solidity Code Completion and Repair [51.0686873716938]
  コード補完モデルによって生成されたSolidityスマートコントラクトの機能的正しさを評価するベンチマークであるSolBenchを紹介する。 本稿では,スマートコントラクトの機能的正当性を検証するための検索拡張コード修復フレームワークを提案する。 その結果、コード修復と検索技術は、計算コストを削減しつつ、スマートコントラクト完了の正しさを効果的に向上することを示した。
  論文  参考訳（メタデータ） (2025-03-03T01:55:20Z)

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

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