論文の概要: ESBMC: A Survey of Its Evolution, Integration, and Future Directions in Formal Software Verification
- arxiv url: http://arxiv.org/abs/2605.26169v1
- Date: Mon, 25 May 2026 00:18:27 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-05-27 17:51:41.266378
- Title: ESBMC: A Survey of Its Evolution, Integration, and Future Directions in Formal Software Verification
- Title（参考訳）: ESBMC: 形式的ソフトウェア検証における進化,統合,今後の方向性に関する調査
- Authors: Pierre Dantas, Lucas Cordeiro, Waldir Junior,
- 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, 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エージェントとの結合を実現している。
この調査は、ESBMCの当初の設計原則から2025-2026年の最先端までの全軌道を辿り、SV-COMPとTest-Compで43の賞を記録、LSM駆動の自己修復ソフトウェアとループ不変生成の正式な検証バックエンドとしての役割、NVIDIA-OpenSMAフレームワークを通じて統合されたエージェントモデルチェックアーキテクチャを初めて工業展開し、ESBMCを受動的検証バックエンドではなく、ネイティブに自律的な検証カーネルとして確立した。
そして、スケーラビリティ、ニューロシンボリックな検証、反例のインテリジェンス、クロスランゲージな検証、安全基準の遵守、オープンソースのサステナビリティにまたがるオープンな課題に関する、構造化された議題で締めくくります。
関連論文リスト
- 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) - 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) - 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。