論文の概要: From Rocq to Metal: A Pipeline for Formally Verified Microcontroller Firmware

• arxiv url: http://arxiv.org/abs/2606.02651v1
• Date: Sun, 31 May 2026 21:14:54 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-06-03 22:00:04.491691
• Title: From Rocq to Metal: A Pipeline for Formally Verified Microcontroller Firmware
• Title（参考訳）: RocqからMetal: 正式に検証されたマイクロコントローラファームウェアのパイプライン
• Authors: Valentin Bergeron, Karolina Gorna,
• Abstract要約: 本稿では,今日,正式に認証されたファームウェアがいかに実現可能かを示す。 マイクロコントローラ上でRocq抽出スキームを実行するベアメタル継続パススタイル仮想マシン(VM)であるEncore!を開発した。 また、ファームウェアを純粋な状態遷移関数として構成する方法を示し、そのコアをRocqで完全に証明できるようにする。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Enforcing invariants in safety-critical systems is increasingly urgent as AI-generated code becomes widespread. Unfortunately, the runtimes required to support high-level specification languages are too large for most embedded targets. In this article, we show how formally verified firmware is achievable today. We built Encore!, a bare-metal Continuation Passing Style (CPS) virtual machine (VM) that runs Rocq-extracted Scheme on microcontrollers. We also show how to structure firmware as a pure state-transition function, making its core fully provable in Rocq while keeping the unverified host layer constant regardless of firmware complexity. Large Language Model (LLM)-assisted tactic synthesis fits naturally into this workflow: formal theorem statements replace manual code review, allowing AI-generated firmware to prove itself.
• Abstract（参考訳）: AI生成コードが普及するにつれて、安全クリティカルなシステムの不変性を強制することがますます急務になっている。 残念ながら、高レベルの仕様言語をサポートするために必要なランタイムは、ほとんどの組み込みターゲットには大きすぎる。 本稿では,今日,正式に認証されたファームウェアがいかに実現可能かを示す。 We built Encore!, a bare-metal Continuation Passing Style (CPS) virtual machine (VM) that run Rocq- Extracted Scheme on microcontrollers。 また、ファームウェアを純粋な状態遷移関数として構成し、そのコアをRocqで完全に証明可能とし、ファームウェアの複雑さに関わらず、未検証のホスト層を一定に保つ方法を示す。 大言語モデル(LLM)が支援する戦術合成は、このワークフローに自然に適合する。

関連論文リスト

• ChipMATE: Multi-Agent Training via Reinforcement Learning for Enhanced RTL Generation [55.947962672433675]
  ChipMATEは、RTL生成のための最初の自己学習型マルチエージェントフレームワークである。 ChipMATEは産業的な実践に触発され、VerilogエージェントとPythonのリファレンスモデルエージェントをペアにし、相互に出力を検証する。 ChipMATEは、VerilogEval V2で75.0%と80.1%パス@1を4Bと9Bベースモデルで達成している。
  論文  参考訳（メタデータ） (2026-05-13T01:04:21Z)
• Autoformalizing Memory Specifications with Agents [3.897906533095668]
  本稿では,メモリチップ仕様をDRAMPyMLという形式表現にする方法を示す。 これはSystemVerilogアサーション、刺激、機能カバレッジの生成に使用できる。 ベンチマークデータセットであるDRAMBenchもリリースしています。
  論文  参考訳（メタデータ） (2026-04-30T02:01:48Z)
• Residual Context Diffusion Language Models [90.07635240595926]
  Residual Context Diffusion (RCD) は、捨てられたトークン表現をコンテキスト残留に変換し、次のデノイングステップでそれらを注入するモジュールである。 RCDは、最小限の計算オーバーヘッドで、5-10ポイントの精度でフロンティアdLLMを一貫して改善する。
  論文  参考訳（メタデータ） (2026-01-30T13:16:32Z)
• HardSecBench: Benchmarking the Security Awareness of LLMs for Hardware Code Generation [24.138048137437078]
  大規模言語モデル(LLM)は、コード生成のための実用的なハードウェアとファームウェア開発パイプラインに統合されつつある。 この研究ギャップは、現実的な仕様の下でセキュリティ意識を評価するためのベンチマークを設計する動機となります。 我々は、Verilog Registers Transfer Level (RTL)とファームウェアレベルCにまたがる924のタスクからなるベンチマークであるHardSecBenchを紹介し、76のハードウェア関連Common Weaknession (CWE)エントリをカバーしている。
  論文  参考訳（メタデータ） (2026-01-20T11:27:40Z)
• From Completion to Editing: Unlocking Context-Aware Code Infilling via Search-and-Replace Instruction Tuning [81.97788535387286]
  本稿では,エージェントによる検証・編集機構を統一された単一パス推論プロセスに内部化するフレームワークを提案する。 最小限のデータで、SRI-Coderは、ChatモデルがBaseモデルの完了性能を上回ることができる。 FIMスタイルのチューニングとは異なり、SRIは一般的なコーディング能力を保持し、標準のFIMに匹敵する推論遅延を維持する。
  論文  参考訳（メタデータ） (2026-01-19T20:33:53Z)
• SwingArena: Competitive Programming Arena for Long-context GitHub Issue Solving [90.32201622392137]
  We present SwingArena, a competitive evaluation framework for Large Language Models (LLMs)。 従来の静的ベンチマークとは異なり、SwingArenaはLLMをイテレーションとして組み合わせて、テストケースを作成し、継続的インテグレーション(CI)パイプラインを通じてパッチを検証するパッチとレビュアーを生成することで、ソフトウェアのコラボレーションプロセスをモデル化する。
  論文  参考訳（メタデータ） (2025-05-29T18:28:02Z)
• LLM4EDA: Emerging Progress in Large Language Models for Electronic Design Automation [74.7163199054881]
  大規模言語モデル(LLM)は、文脈理解、論理推論、回答生成においてその能力を実証している。 本稿では,EDA分野におけるLLMの応用に関する系統的研究を行う。 論理合成,物理設計,マルチモーダル特徴抽出,回路のアライメントにLLMを適用することに焦点を当て,今後の研究の方向性を強調した。
  論文  参考訳（メタデータ） (2023-12-28T15:09:14Z)
• AIM: Automatic Interrupt Modeling for Dynamic Firmware Analysis [14.623460803437057]
  AIMは汎用的でスケーラブルで、ハードウェアに依存しない動的ファームウェア分析フレームワークである。 AIMは、ファームウェアにおける割り込み依存コードを、新しい、ファームウェア誘導のジャスト・イン・タイム・イン・タイム・イン・タイム・インターファイリング技術によってカバーする。 私たちのフレームワークは、最先端のアプローチよりも11.2倍の割り込み依存のコードをカバーしています。
  論文  参考訳（メタデータ） (2023-12-02T18:06:22Z)
• HIVE: Scalable Hardware-Firmware Co-Verification using Scenario-based Decomposition and Automated Hint Extraction [2.977255700811213]
  ハードウェア確認ソフトの共検証は、信頼できるシステムの設計に不可欠である。 ハードウェアを手動で抽象化したり、ヒントを手動で生成することで、ファームウェア検証中の状態空間を削減できる有望な方法がある。 本稿では,シミュレーションに基づく検証のスケーラビリティと形式検証の完全性とを効果的に組み合わせる。
  論文  参考訳（メタデータ） (2023-09-14T19:24:57Z)

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

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