論文の概要: ESBMC: A Survey of Its Evolution, Integration, and Future Directions in Formal Software Verification

• arxiv url: http://arxiv.org/abs/2605.26169v2
• Date: Sat, 30 May 2026 20:58:19 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-06-02 18:24:16.437452
• Title: ESBMC: A Survey of Its Evolution, Integration, and Future Directions in Formal Software Verification
• Title（参考訳）: ESBMC: 形式的ソフトウェア検証における進化,統合,今後の方向性に関する調査
• Abstract要約: この調査は、ESBMCの当初の設計原則から2025-2026年の最先端まで、完全な軌道を辿っている。 我々は、その経済的な影響 - GBP 9.3百万ドル、EUR 4.98百万ドル - を、確認された公的研究資金、VeriBeeのスピンオフ、ロッキード・マーティンの防衛産業展開で合成する。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: The Efficient SMT-Based Context-Bounded Model Checker (ESBMC) has grown from a research prototype for verifying embedded ANSI-C software into one of the most versatile and industrially capable formal verification platforms available today. Since its first publication in 2009, ESBMC has undergone persistent evolution: expanding its verification techniques, widening its language support to nine front-ends, integrating industrial-strength SMT solvers, and - most recently - coupling with Large Language Models (LLMs) and autonomous AI agents. This survey traces the full trajectory of ESBMC from its original design principles to the state of the art in 2025-2026, documenting 43 awards at SV-COMP and Test-Comp, peer recognition at leading software engineering venues, including a Distinguished Paper Awards at ICSE'11 and ASE'24, a Most Influential Paper Award at ASE'23, and a Best Tool Paper Award at SBSeg'23, its role as a formal verification backend for LLM-driven self-healing software and loop invariant generation, and the first industrial deployment of an integrated agentic model-checking architecture through the NVIDIA-OpenSMA framework, establishing ESBMC as a natively autonomous verification kernel rather than a passive validation backend. We synthesize its economic impact - over GBP 9.3 million and EUR 4.98 million in confirmed public research funding, the VeriBee spin-off, and a defense industrial deployment at Lockheed Martin - and conclude with a structured agenda of open challenges spanning scalability, neurosymbolic verification, counterexample intelligibility, cross-language verification, safety standards compliance, and open-source sustainability.
• Abstract（参考訳）: ESBMC(Efficient SMT-based Context-Bounded Model Checker)は、組み込みANSI-Cソフトウェアを検証するための研究のプロトタイプから、今日入手可能な最も汎用的で工業的に実行可能な形式的検証プラットフォームへと成長した。 2009年の最初の出版以来、ESBMCは永続的な進化を遂げている。検証技術を拡大し、言語サポートを9つのフロントエンドに拡大し、産業力のあるSMTソルバを統合し、そして最近では、大規模言語モデル(LLM)と自律AIエージェントとの結合を実現している。 この調査は、最初の設計原則から2025-2026年の最先端まで、ESBMCの完全な軌道を辿り、SV-COMPとTest-Compで43の賞を記録、ICSE'11とASE'24で傑出した論文賞、ASE'23でもっとも影響力のある論文賞、SBSeg'23で最高のツール論文賞、LLM駆動の自己修復ソフトウェアとループ不変世代の公式な検証バックエンドとしての役割、NVIDIA-OpenSMAフレームワークを通じて統合されたエージェントモデルチェックアーキテクチャを初めて工業的に展開した。 そして、スケーラビリティ、ニューロシンボリックな検証、反例のインテリジェンス、クロスランゲージな検証、安全基準の遵守、オープンソースのサステナビリティにまたがるオープンな課題に関する、構造化された議題で締めくくります。

関連論文リスト

• FormalTCS: Benchmarking End-to-End Frontier Formal Theoretical Computer Science Research of Large Language Models [53.68149869349268]
  大規模言語モデル(LLM)は、自動理論計算機科学(TCS)研究の可能性を増大させている。 我々は、最前線のエンドツーエンドのTCS研究でLSMを評価するための専門家検証ベンチマークである ourbenchmarkを紹介した。
  論文  参考訳（メタデータ） (2026-08-20T15:13:41Z)
• A Sovereign, Open-Source Foundation Model for German and English [50.08096276509294]
  Soofi S 30B-A3B(ソフィー S 30B-A3B)は、ドイツのマムバ・トランスフォーマー・ファウンデーション・モデルである。 そのハイブリッド設計はトークン毎に30Bパラメータの3Bのみを起動し、コンテキストが大きくなるにつれて推論キャッシュをほぼ一定に保ちます。
  論文  参考訳（メタデータ） (2026-07-10T13:51:41Z)
• Plan First, Judge Later, Run Better: A DMAIC-Inspired Agentic System for Industrial Anomaly Detection [51.90293101535452]
  本稿では, DMAIC-IAD (DMAIC-inspired Agentic Industrial Anomaly Detection) というマルチエージェントシステムを提案する。 DMAIC-IADは,適用対象のエージェントベースラインに対する平均検出性能を37.76%向上させる。
  論文  参考訳（メタデータ） (2026-06-03T08:38:14Z)
• From CRUD to Autonomous Agents: Formal Validation and Zero-Trust Security for Semantic Gateways in AI-Native Enterprise Systems [0.0]
  本稿では,モデルコンテキストプロトコル(MCP)が管理するセマンティックゲートウェイの設計,形式検証,実証評価を提案する。 ゲートウェイは、エンタプライズAPIをセマンティックサーフェスとして再構成する。 このアーキテクチャでは、事前に推論されたセマンティックファイアウォール、決定論的ツールレベルRBAC、アウトオブバンドの暗号化人間対ループの承認を含む3層ゼロトラストセキュリティモデルが導入されている。
  論文  参考訳（メタデータ） (2026-04-28T12:25:06Z)
• Towards Agentic Test-Driven Quality Assurance for 6G Networks [0.0]
  テスト駆動品質保証パラダイムとインテントコクリエーションを統合したエージェント型、インテント駆動のエンドツーエンド(E2E)オーケストレーションフレームワークを提案する。 このアーキテクチャは、TMフォーラムの情報モデルとカタログを使用して、標準に準拠した知識表現に基づいている。
  論文  参考訳（メタデータ） (2026-04-25T12:58:36Z)
• Detecting Corporate AI-Washing via Cross-Modal Semantic Inconsistency Learning [0.0]
  本稿では,AI洗浄検出を再定義するフレームワークであるAWASHについて,モーダルなクレームエビデンス推論として紹介する。 本稿では,クレーム・エビデンス関連推論のための構造化自然言語推論モジュールであるトリモーダルエンコーダを統合する,CMID(Cross-Modal Inconsistency Detection)ネットワークを提案する。 CMIDはF1スコアが0.882、AUC-ROCが0.921であり、テキストのみのベースラインが17.4ポイント、最新のマルチモーダル・コンペティターが11.3ポイントを上回っている。
  論文  参考訳（メタデータ） (2026-03-24T01:30:36Z)
• Operationalising Artificial Intelligence Bills of Materials (AIBOMs) for Verifiable AI Provenance and Lifecycle Assurance [11.812618112854116]
  本研究では,CycloneDX規格を拡張したAIBOM(Artificial Intelligence Bill of Materials)スキーマを提案する。 自律型AIパイプラインは、継続的環境検査、脆弱性の強化、マシンが検証可能な前兆チェーンを使用した監査を実行するために開発されている。
  論文  参考訳（メタデータ） (2026-03-17T20:45:09Z)
• SWE-Universe: Scale Real-World Verifiable Environments to Millions [84.63665266236963]
  SWE-Universeは、GitHubのプルリクエスト(PR)から検証可能な環境を自動的に構築するフレームワークである。 本稿では, 自動建築の課題を克服するために, 効率的なカスタムトレーニングモデルを用いた建築エージェントを提案する。 大規模エージェントによる中等教育と強化学習を通じて,環境の重要さを実証する。
  論文  参考訳（メタデータ） (2026-02-02T17:20:30Z)
• AI-NativeBench: An Open-Source White-Box Agentic Benchmark Suite for AI-Native Systems [52.65695508605237]
  我々は、Model Context Protocol(MCP)とAgent-to-Agent(A2A)標準に基づいて、アプリケーション中心でホワイトボックスのAI-NativeベンチマークスイートであるAI-NativeBenchを紹介する。 エージェントスパンを分散トレース内の第一級市民として扱うことにより,本手法は,単純な機能以上の工学的特性の粒度解析を可能にする。 この研究は、モデル能力の測定から信頼性の高いAI-Nativeシステムへの移行を導く最初の体系的な証拠を提供する。
  論文  参考訳（メタデータ） (2026-01-14T11:32:07Z)
• BarrierBench : Evaluating Large Language Models for Safety Verification in Dynamical Systems [4.530582224312311]
  バリア証明書合成のための LLM ベースのエージェントフレームワークを提案する。 このフレームワークは自然言語推論を使用して、候補証明書を提案し、洗練し、検証する。 BarrierBenchは、線形、非線形、離散時間、連続時間設定にまたがる100の動的システムのベンチマークである。
  論文  参考訳（メタデータ） (2025-11-12T14:23:49Z)
• Cognitive Kernel-Pro: A Framework for Deep Research Agents and Agent Foundation Models Training [67.895981259683]
  汎用AIエージェントは、次世代人工知能の基礎となるフレームワークとして、ますます認識されている。 現在のエージェントシステムはクローズドソースか、さまざまな有料APIやプロプライエタリなツールに大きく依存している。 我々は,完全オープンソースかつ(最大限に)フリーなマルチモジュールエージェントフレームワークであるCognitive Kernel-Proを提案する。
  論文  参考訳（メタデータ） (2025-08-01T08:11:31Z)
• Zero-Trust Foundation Models: A New Paradigm for Secure and Collaborative Artificial Intelligence for Internet of Things [61.43014629640404]
  Zero-Trust Foundation Models (ZTFM)は、ゼロトラストセキュリティの原則をIoT(Internet of Things)システムの基盤モデル(FM)のライフサイクルに組み込む。 ZTFMは、分散、異質、潜在的に敵対的なIoT環境にわたって、セキュアでプライバシ保護のAIを可能にする。
  論文  参考訳（メタデータ） (2025-05-26T06:44:31Z)
• Benchmarking Multi-modal Semantic Segmentation under Sensor Failures: Missing and Noisy Modality Robustness [61.87055159919641]
  マルチモーダルセマンティックセグメンテーション(MMSS)は、モーダル間で補完情報を統合することで、単一モーダルデータの制限に対処する。 顕著な進歩にもかかわらず、マルチモーダルデータ品質の変動と不確実性により、研究と実世界の展開の間に大きなギャップが持続する。 Intire-Missing Modality (EMM)、Random-Missing Modality (RMM)、Noisy Modality (NM)の3つのシナリオでMMSSモデルを評価する頑健性ベンチマークを導入する。
  論文  参考訳（メタデータ） (2025-03-24T08:46:52Z)
• The Dual-use Dilemma in LLMs: Do Empowering Ethical Capacities Make a Degraded Utility? [54.18519360412294]
  大きな言語モデル(LLM)は、安全のための有害な要求を拒否することと、ユーティリティのための正当な要求を収容することのバランスをとる必要がある。 本稿では,DPO(Direct Preference Optimization)に基づくアライメントフレームワークを提案する。 我々は,DeepSeek-R1をベンチマークでテストした結果を解析し,この高い評価を得たモデルがもたらす批判的倫理的懸念を明らかにする。
  論文  参考訳（メタデータ） (2025-01-20T06:35:01Z)
• Verifying components of Arm(R) Confidential Computing Architecture with ESBMC [6.914213030256384]
  Realm Management Monitor (RMM) はArm Confidential Computing Architecture (Arm CCA) において重要なファームウェアコンポーネントである これまでの研究は、RMMの仕様とプロトタイプ参照実装の検証に形式的検証技術を適用していた。 本稿では,SMT(Satifiability Modulo Theories)ベースのソフトウェアモデルチェッカーであるESBMCの適用について述べる。
  論文  参考訳（メタデータ） (2024-06-05T09:09:37Z)
• A New Era in Software Security: Towards Self-Healing Software via Large Language Models and Formal Verification [8.733354577147093]
  本稿では,Large Language Models(LLM)とFormal Verification戦略を組み合わせたソフトウェア脆弱性の自動修復手法を提案する。 我々は、ESBMC-AIフレームワークを概念実証として、よく認識され、業界に受け入れられたSMTベースのコンテキスト境界モデルチェッカー(ESBMC)と事前訓練されたトランスフォーマーモデルを活用する。 本研究は,バッファオーバーフローや演算オーバーフロー,ポインタ参照障害などの問題を高精度に検出および修正するESBMC-AIの機能を示すものである。
  論文  参考訳（メタデータ） (2023-05-24T05:54:10Z)

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

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