論文の概要: Kani: A Model Checker for Rust

• arxiv url: http://arxiv.org/abs/2607.01504v1
• Date: Wed, 01 Jul 2026 22:05:33 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-07-03 19:45:08.605043
• Title: Kani: A Model Checker for Rust
• Title（参考訳）: Kani: Rustのモデルチェッカー
• Authors: Rémi Delmas, Zyad Hassan, Qinheping Hu, Rahul Kumar, Felipe R. Monteiro, Thanh Nguyen, Adrián Palacios, Celina Val, Michael Tautschnig, Justus Adam, Daniel Schwartz-Narbonne, Carolyn Zech,
• Abstract要約: KaniはRustのオープンソースモデルチェッカーである。 バグフィニング以外のバウンドモデルチェックをプッシュして、正確性を保証する。 KaniはプロダクションCIで大規模に運用されており、コード変更毎に16,000以上のハーネスが検証されている。
• 参考スコア（独自算出の注目度）: 3.019677299390329
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Rust's ownership type system prevents memory errors in safe code, but certain desirable properties remain orthogonal to compilation: the soundness of unsafe operations (e.g., raw pointer dereferences), functional correctness, and absence of runtime panics. We present Kani, an open-source model checker for Rust that pushes bounded model checking beyond bug-finding to provide correctness guarantees for these properties. Kani compiles proof harnesses from Rust's Mid-level Intermediate Representation (MIR) into CBMC's bit-precise verification engine, automatically checking a comprehensive set of safety properties with no user annotation. To extend verification from bounded to unbounded, Kani provides a specification language comprising function contracts, loop contracts, quantifiers, and function stubbing. We demonstrate feasibility through case studies on industrial Rust projects, where contracts upgraded verification from panic-freedom to functional correctness, uncovering six previously unknown bugs. Kani operates at scale in production CI, with over 16,000 harnesses verified per code change in the Rust standard library verification campaign.
• Abstract（参考訳）: Rustのオーナシップ型システムは、安全なコードにおけるメモリエラーを防止するが、特定の望ましいプロパティはコンパイルに直交している。 これはRust用のオープンソースのモデルチェッカーで、バウンダリモデルチェックをバグフィニングを越えてプッシュすることで、これらのプロパティの正確性を保証する。 Kaniは、RustのMid-level Intermediate Representation (MIR)からCBMCのビット精度検証エンジンにエビデンスハーネスをコンパイルし、ユーザアノテーションなしで包括的な安全プロパティのセットを自動的にチェックする。 有界から非有界への検証を拡張するため、Kaniは関数コントラクト、ループコントラクト、定量化器、関数スタブを含む仕様言語を提供する。 我々は産業用Rustプロジェクトのケーススタディを通じて、パニックフリーダムから機能的正当性への検証をコントラクトでアップグレードし、6つの既知のバグを発見できる可能性を示します。 Kaniは運用レベルのCIで大規模に運用されており、Rust標準ライブラリ検証キャンペーンのコード変更毎に16,000以上のハーネスが検証されている。

関連論文リスト

• Verifying the Rust Standard Library [3.303009078327922]
  Rustの型システムは、多くのメモリエラーのクラスを防ぐが、標準ライブラリは安全でないコードに大きく依存している。 これは、補完的な検証ツールをRust標準ライブラリからフォークされた検証リポジトリの継続的統合に統合する、オープンでクラウドソースされた取り組みです。
  論文  参考訳（メタデータ） (2026-06-16T00:11:04Z)
• Agentic Model Checking [12.832868209928039]
  本稿では,LLMエージェントと境界モデルチェックバックエンドを結合するパラダイムを提案する。 我々は、BMC-Agentのアプローチをインスタンス化し、CとRustのLLM生成カーネルおよびコンパイラコード上で評価する。
  論文  参考訳（メタデータ） (2026-05-20T17:25:52Z)
• The Hidden Signal of Verifier Strictness: Controlling and Improving Step-Wise Verification via Selective Latent Steering [67.8271652641864]
  我々は,隠蔽状態の介入によって検証の厳密性を制御できるかどうかを検討した。 VerifySteerは、サンプルレベルのルーティングに潜時補正信号を使用し、段落境界に選択的に介入する。
  論文  参考訳（メタデータ） (2026-05-20T05:48:16Z)
• CRUST-Bench: A Comprehensive Benchmark for C-to-safe-Rust Transpilation [51.18863297461463]
  CRUST-Benchは100のCリポジトリのデータセットで、それぞれが安全なRustとテストケースで手書きのインターフェースとペアリングされている。 我々は、このタスクで最先端の大規模言語モデル(LLM)を評価し、安全で慣用的なRust生成が依然として難しい問題であることを確認した。 最高のパフォーマンスモデルであるOpenAI o1は、ワンショット設定で15タスクしか解決できない。
  論文  参考訳（メタデータ） (2025-04-21T17:33:33Z)
• Automated Proof Generation for Rust Code via Self-Evolution [69.25795662658356]
  私たちは、Rustコードの自動証明生成を可能にする、人書きスニペットの欠如を克服するフレームワークであるSAFEを紹介します。 SAFEは、細調整されたモデルの自己老化能力を訓練するために、多数の合成不正確な証明を再利用する。 我々は、人間の専門家によるベンチマークで52.52%の精度で達成し、GPT-4oのパフォーマンス14.39%を大きく上回った。
  論文  参考訳（メタデータ） (2024-10-21T08:15:45Z)
• Yuga: Automatically Detecting Lifetime Annotation Bugs in the Rust Language [15.164423552903571]
  Rustプロジェクトでは、セキュリティ上の脆弱性が報告されている。 これらの脆弱性は、部分的には関数シグネチャの誤った終身アノテーションから生じます。 既存のツールはこれらのバグを検出するのに失敗する。 我々は,新たな静的解析ツールであるYugaを考案し,潜在的なライフタイムアノテーションのバグを検出する。
  論文  参考訳（メタデータ） (2023-10-12T17:05:03Z)

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

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