論文の概要: Multi-Threaded Software Model Checking via Parallel Trace Abstraction Refinement

• arxiv url: http://arxiv.org/abs/2509.13699v1
• Date: Wed, 17 Sep 2025 05:05:16 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-09-18 18:41:50.722559
• Title: Multi-Threaded Software Model Checking via Parallel Trace Abstraction Refinement
• Title（参考訳）: 並列トレース抽象化によるマルチスレッドソフトウェアモデルチェック
• Authors: Max Barth, Marie-Christine Jakobs,
• Abstract要約: 本稿では,ソフトウェアモデル検査における抽象的手法であるトレース抽象化を並列化する手法を提案する。 我々のアプローチは、抽象化ベースのソフトウェアモデルチェックに対する最近の並列アプローチであるDSSよりも効果的です。
• 参考スコア（独自算出の注目度）: 1.955166888058497
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Automatic software verification is a valuable means for software quality assurance. However, automatic verification and in particular software model checking can be time-consuming, which hinders their practical applicability e.g., the use in continuous integration. One solution to address the issue is to reduce the response time of the verification procedure by leveraging today's multi-core CPUs. In this paper, we propose a solution to parallelize trace abstraction, an abstraction-based approach to software model checking. The underlying idea of our approach is to parallelize the abstraction refinement. More concretely, our approach analyzes different traces (syntactic program paths) that could violate the safety property in parallel. We realize our parallelized version of trace abstraction in the verification tool Ulti mate Automizer and perform a thorough evaluation. Our evaluation shows that our parallelization is more effective than sequential trace abstraction and can provide results significantly faster on many time-consuming tasks. Also, our approach is more effective than DSS, a recent parallel approach to abstraction-based software model checking.
• Abstract（参考訳）: 自動ソフトウェア検証は、ソフトウェア品質保証にとって貴重な手段である。 しかし、自動検証や特にソフトウェアモデルチェックは時間がかかり、例えば継続的インテグレーションでの使用が現実的な適用性を妨げます。 この問題に対処する解決策の1つは、今日のマルチコアCPUを活用することで、検証手順の応答時間を削減することである。 本稿では,ソフトウェアモデル検査における抽象的手法であるトレース抽象化を並列化する手法を提案する。 このアプローチの根底にある考え方は、抽象化の洗練を並列化することです。 より具体的には、我々のアプローチは、並列に安全性を損なう可能性のある異なるトレース(シンタクティックプログラムパス)を分析します。 検証ツールUlti mate Automizerにおけるトレース抽象化の並列化バージョンを実現し、徹底的な評価を行う。 評価の結果、並列化は逐次トレースの抽象化よりも効果的であり、多くの時間を要するタスクにおいて結果が大幅に高速であることがわかった。 また、近年の抽象化ベースのソフトウェアモデルチェックに対する並列アプローチであるDSSよりも、当社のアプローチの方が効果的です。

関連論文リスト

• SPARE: Single-Pass Annotation with Reference-Guided Evaluation for Automatic Process Supervision and Reward Modelling [58.05959902776133]
  私たちはSingle-Passを紹介します。 Reference-Guided Evaluation (SPARE)は、効率的なステップごとのアノテーションを可能にする新しい構造化フレームワークである。 数学的推論(GSM8K, MATH)、マルチホップ質問応答(MuSiQue-Ans)、空間推論(SpaRP)にまたがる4つの多様なデータセットにおけるSPAREの有効性を実証する。 ProcessBenchでは、SPAREがデータ効率のよいアウト・オブ・ディストリビューションの一般化を実証し、トレーニングサンプルの$sim$16%しか使用していない。
  論文  参考訳（メタデータ） (2025-06-18T14:37:59Z)
• Structural Abstraction and Selective Refinement for Formal Verification [0.5735035463793008]
  ロボットアプリケーションの安全性検証は、ロボットが通常操作する環境の複雑さのため、非常に難しい。 通常のソリューションアプローチは抽象化であり、より正確に振る舞いの抽象化です。 そこで我々は,ロボット環境のボクセル表現の文脈において,構造的抽象化を提案する。
  論文  参考訳（メタデータ） (2025-05-29T01:44:47Z)
• Thinking Longer, Not Larger: Enhancing Software Engineering Agents via Scaling Test-Time Compute [61.00662702026523]
  より大規模なモデルではなく、推論時間の増加を活用する統合されたテスト時間計算スケーリングフレームワークを提案する。 当社のフレームワークには,内部TTCと外部TTCの2つの補完戦略が組み込まれている。 当社の textbf32B モデルは,DeepSeek R1 671B や OpenAI o1 など,はるかに大きなモデルを上回る 46% の課題解決率を実現している。
  論文  参考訳（メタデータ） (2025-03-31T07:31:32Z)
• A Case Study on Model Checking and Runtime Verification for Awkernel [0.7199733380797578]
  人間が手動で同時動作をレビューしたり、可能なすべての実行をカバーしたテストケースを書くことは難しい。 本稿では,スケジューラなどの並列ソフトウェアの開発手法を提案する。
  論文  参考訳（メタデータ） (2025-03-12T11:27:45Z)
• Code Review Automation Via Multi-task Federated LLM -- An Empirical Study [4.8342038441006805]
  本研究は,2つの逐次法,1つの並列法,2つの累積法を含む,マルチタスクトレーニングのための5つの簡単な手法について検討した。 その結果,フェデレートされたLLM(FedLLM)をコードレビューのマルチタスクのユースケースで逐次トレーニングすることは,タスク毎に個別のモデルをトレーニングするよりも,時間,計算,パフォーマンスの指標の面で効率が低いことが示唆された。
  論文  参考訳（メタデータ） (2024-12-20T08:46:46Z)
• Step-by-Step Reasoning for Math Problems via Twisted Sequential Monte Carlo [55.452453947359736]
  Twisted Sequential Monte Carlo(TSMC)に基づく新しい検証手法を提案する。 TSMCを大規模言語モデルに適用し、部分解に対する将来的な報酬を推定する。 このアプローチは、ステップワイドなヒューマンアノテーションを必要としない、より直接的なトレーニングターゲットをもたらす。
  論文  参考訳（メタデータ） (2024-10-02T18:17:54Z)
• Transformer-based assignment decision network for multiple object tracking [2.2920634931825803]
  本稿では,データアソシエーションに取り組むトランスフォーマーベースのアサインメント決定ネットワーク(TADN)について,推論中に明示的な最適化を必要とせずに紹介する。 提案手法は,トラッカーとしての単純な性質にもかかわらず,ほとんどの評価指標において高い性能を示す。
  論文  参考訳（メタデータ） (2022-08-06T19:47:32Z)
• Parallel and Multi-Objective Falsification with Scenic and VerifAI [11.152087017964584]
  シナリオ仕様言語とVerifAIツールキットの拡張について述べる。 まず,Scanicのシミュレーションとサンプリング機能の両方にインタフェースを組み込んだ並列化フレームワークを提案する。 次に、サンプリング中の多目的最適化をサポートするために、VerifAIのファルシフィケーションアルゴリズムの拡張を示す。
  論文  参考訳（メタデータ） (2021-07-09T01:08:49Z)

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

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