論文の概要: Software Model Checking via Summary-Guided Search (Extended Version)

• arxiv url: http://arxiv.org/abs/2508.15137v3
• Date: Mon, 08 Sep 2025 23:15:20 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-09-10 14:38:26.92096
• Title: Software Model Checking via Summary-Guided Search (Extended Version)
• Title（参考訳）: 概要ガイド検索によるソフトウェアモデル検査(拡張版)
• Authors: Ruijie Fang, Zachary Kincaid, Thomas Reps,
• Abstract要約: GPSは、プログラムチェックのタスクを、プログラム状態の直接検索として扱う。 GPSは安全性の証明と、安全性に対する反例の両方を見つけることができる。 GPSは、長い入力依存のエラーパスを含むプログラムでバグを見つけることができる。
• 参考スコア（独自算出の注目度）: 0.573723069267867
• License: http://creativecommons.org/licenses/by-nc-sa/4.0/
• Abstract: In this work, we describe a new software model-checking algorithm called GPS. GPS treats the task of model checking a program as a directed search of the program states, guided by a compositional, summary-based static analysis. The summaries produced by static analysis are used both to prune away infeasible paths and to drive test generation to reach new, unexplored program states. GPS can find both proofs of safety and counter-examples to safety (i.e., inputs that trigger bugs), and features a novel two-layered search strategy that renders it particularly efficient at finding bugs in programs featuring long, input-dependent error paths. To make GPS refutationally complete (in the sense that it will find an error if one exists, if it is allotted enough time), we introduce an instrumentation technique and show that it helps GPS achieve refutation-completeness without sacrificing overall performance. We benchmarked GPS on a diverse suite of benchmarks including programs from the Software Verification Competition (SV-COMP), from prior literature, as well as synthetic programs based on examples in this paper. We found that our implementation of GPS outperforms state-of-the-art software model checkers (including the top performers in SV-COMP ReachSafety-Loops category), both in terms of the number of benchmarks solved and in terms of running time.
• Abstract（参考訳）: 本稿では,GPSと呼ばれる新しいソフトウェアモデルチェックアルゴリズムについて述べる。 GPSは、プログラムチェックのタスクを、構成的、要約に基づく静的解析によってガイドされたプログラム状態の直接探索として扱う。 静的解析によって生成された要約は、実現不可能なパスを抽出し、新しい未探索プログラム状態に到達するためにテスト生成を駆動するために使用される。 GPSは安全性の証明と、安全性の反例(つまりバグを引き起こす入力)の両方を見つけることができ、また、長い入力依存のエラーパスを持つプログラムのバグを見つけるのに特に効率的である、新しい2層検索戦略を特徴としている。 本研究は,GPSの消火性能を向上させるため,GPSの消火性能を損なうことなく,GPSの消火性能を向上させる手法を提案する。 我々は,従来の文献からのソフトウェア検証コンペティション(SV-COMP)プログラムや,本論文の例に基づく合成プログラムを含む,多様なベンチマークでGPSをベンチマークした。 我々は,最新のソフトウェアモデルチェッカー(SV-COMP ReachSafety-Loopsカテゴリのトップパフォーマーを含む)よりも,ベンチマーク数や実行時間の両面で,GPSの実装が優れていることを確認した。

関連論文リスト

• Plane Geometry Problem Solving with Multi-modal Reasoning: A Survey [8.887710491315088]
  平面幾何学的問題解決(PGPS)は近年,大規模視覚言語モデルのマルチモーダル推論能力を評価するベンチマークとして注目されている。 PGPSへの関心が高まりつつあるにもかかわらず、研究コミュニティはPGPSの最近の研究を体系的に合成する包括的な概要を欠いている。 我々はまず,PGPS手法をエンコーダ・デコーダ・フレームワークに分類し,それらのエンコーダとデコーダが使用する出力形式を要約する。
  論文  参考訳（メタデータ） (2025-05-20T13:27:17Z)
• TrustGeoGen: Scalable and Formal-Verified Data Engine for Trustworthy Multi-modal Geometric Problem Solving [66.0201510984171]
  問題生成のためのスケーラブルなデータエンジンTrustGeoGenを提案する。 正式な検証により、TrustGeoGenは、モダリティの整合性を保証するGeoTrust-200Kデータセットを生成する。 実験の結果、GeoTrust-testの精度は49.17%に過ぎなかった。
  論文  参考訳（メタデータ） (2025-04-22T10:45:23Z)
• GPS-IDS: An Anomaly-based GPS Spoofing Attack Detection Framework for Autonomous Vehicles [1.1992484839577393]
  GPSネットワークは、偽造や妨害といったサイバー攻撃に弱い。 本稿では,異常な侵入検知フレームワークであるGPS-IDSを提案する。 私たちの知る限りでは、このデータセットはこの種のデータセットとしては初めてのもので、このようなセキュリティ上の課題に対処するために、グローバルな研究コミュニティが公開している。
  論文  参考訳（メタデータ） (2024-05-14T06:55:16Z)
• RTracker: Recoverable Tracking via PN Tree Structured Memory [71.05904715104411]
  本稿では,木構造メモリを用いてトラッカーと検出器を動的に関連付け,自己回復を可能にするRTrackerを提案する。 具体的には,正負と負のターゲットサンプルを時系列に保存し,維持する正負のツリー構造メモリを提案する。 我々の中核となる考え方は、正と負の目標カテゴリーの支持サンプルを用いて、目標損失の信頼性評価のための相対的距離に基づく基準を確立することである。
  論文  参考訳（メタデータ） (2024-03-28T08:54:40Z)
• Tracking with Human-Intent Reasoning [64.69229729784008]
  この作業では、新しいトラッキングタスクであるインストラクショントラッキングを提案している。 ビデオフレーム内で自動的にトラッキングを実行するようにトラッカーに要求する暗黙の追跡命令を提供する。 TrackGPTは複雑な推論ベースの追跡を行うことができる。
  論文  参考訳（メタデータ） (2023-12-29T03:22:18Z)
• Leveraging Driver Field-of-View for Multimodal Ego-Trajectory Prediction [69.29802752614677]
  RouteFormerは、GPSデータ、環境コンテキスト、運転者の視野を組み合わせた新しいエゴ軌道予測ネットワークである。 データ不足に対処し、多様性を高めるために、同期運転場と視線データに富んだ都市運転シナリオのデータセットであるGEMを導入する。
  論文  参考訳（メタデータ） (2023-12-13T23:06:30Z)
• TAPIR: Tracking Any Point with per-frame Initialization and temporal Refinement [64.11385310305612]
  本稿では,ビデオシーケンスを通して任意の物理面上の問合せ点を効果的に追跡する,TAP(Tracking Any Point)の新しいモデルを提案する。 提案手法では,(1)他のフレームの問合せ点に対する適切な候補点マッチングを独立に特定するマッチング段階と,(2)局所的相関に基づいてトラジェクトリと問合せの両方を更新する改良段階の2段階を用いる。 結果として得られたモデルは、DAVISにおける平均約20%の絶対平均ジャカード(AJ)改善によって示されるように、TAP-Vidベンチマークにおける大きなマージンで、すべてのベースライン手法を上回ります。
  論文  参考訳（メタデータ） (2023-06-14T17:07:51Z)
• Unsupervised Visual Odometry and Action Integration for PointGoal Navigation in Indoor Environment [14.363948775085534]
  屋内環境におけるポイントゴールナビゲーションは、個人ロボットが特定の地点に向かうための基本的なタスクである。 GPS信号を使わずにPointGoalナビゲーションの精度を向上させるために、ビジュアル・オドメトリー(VO)を用い、教師なしで訓練された新しいアクション統合モジュール(AIM)を提案する。 実験により,提案システムは良好な結果が得られ,Gibsonデータセット上で部分的に教師付き学習アルゴリズムよりも優れていた。
  論文  参考訳（メタデータ） (2022-10-02T03:12:03Z)
• Benchmarking high-fidelity pedestrian tracking systems for research, real-time monitoring and crowd control [55.41644538483948]
  実生活環境における高忠実な歩行者追跡は,群集動態研究において重要なツールである。 この技術が進歩するにつれて、社会においても益々有用になってきている。 歩行者追跡技術の研究と技術に成功させるためには、正確さの検証とベンチマークが不可欠である。 我々は、プライバシーに配慮した歩行者追跡技術のためのベンチマークスイートをコミュニティのオープンスタンダードに向けて提示し、議論する。
  論文  参考訳（メタデータ） (2021-08-26T11:45:26Z)
• Learning Low-Correlation GPS Spreading Codes with a Policy Gradient Algorithm [2.741266294612776]
  コード系列を拡散する高品質なファミリを構成する強化学習アルゴリズムを開発した。 著者の知識を最大限に活用するため、これは機械学習/強化学習アプローチを使用してナビゲーション拡散コードを設計する最初の仕事である。
  論文  参考訳（メタデータ） (2021-01-08T04:53:11Z)

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

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