論文の概要: Improving Debugging in Verification-Aware Languages Through Automated Fault Localization: A Case Study in Dafny

• arxiv url: http://arxiv.org/abs/2608.05399v2
• Date: Fri, 07 Aug 2026 14:31:04 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-08-10 14:11:31.088926
• Title: Improving Debugging in Verification-Aware Languages Through Automated Fault Localization: A Case Study in Dafny
• Title（参考訳）: 自動フォールトローカライゼーションによる検証対象言語でのデバッグ改善:Dafnyを事例として
• Authors: Álvaro Silva, Isabel Amaral, João Pascoal Faria, Alexandra Mendes,
• Abstract要約: 本稿では,検証対応言語の自動故障位置決めについて検討する。 状態ベースと反例ベースのローカライゼーションの2つのパラダイムを比較した。 以上の結果から, 反例に基づくアプローチは, この設定における状態ベースローカライゼーションを著しく上回っていることがわかった。
• 参考スコア（独自算出の注目度）: 40.61088147738459
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Verification-aware languages, like Dafny, integrate formal specifications directly into source code to enable static correctness checks. However, when verification fails, the feedback provided is often limited to the specific condition of the error, such as a violated postcondition, rather than the root cause of the fault. While Dafny's counterexample features provide concrete execution traces, these typically expose a single failing path per assertion failure, leaving the developer to manually look through the entire trace to locate the error. This paper investigates automated fault localization for verification-aware languages by comparing two paradigms: state-based and counterexample-based localization. Our state-based localization strategy replicates the ``snapshot'' methodology of AutoFix by inferring invariants and predicates to identify suspicious program states. The counterexample-based strategy consists of a family of techniques that progressively enrich the use of verifier output: from raw counterexample extraction, to structured single-trace ranking, and to multi-trace aggregation. To validate these methods, we present an evaluation framework using MutDafny to generate a diverse mutant dataset from DafnyBench and measure localization effectiveness using the EXAM score. Our results show that counterexample-based approaches substantially outperform state-based localization in this setting. Structured ranking over a single trace yields the largest improvement over raw counterexample output, while multi-trace aggregation provides additional gains in robustness and debugging utility by increasing coverage and reducing path bias introduced by the solver. These findings demonstrate that effective fault localization in verification-aware languages depends both on using counterexample information, and how that information is structured and diversified.
• Abstract（参考訳）: Dafnyのような検証対応言語は、公式仕様を直接ソースコードに統合し、静的な正当性チェックを可能にする。 しかしながら、検証が失敗した場合、提供されたフィードバックは、障害の根本原因ではなく、違反した事後条件のようなエラーの特定の条件に制限されることが多い。 Dafnyの反例機能は具体的な実行トレースを提供するが、これらは通常、アサーション障害毎に単一の障害パスを公開するため、開発者は手動でトレース全体を調べてエラーを見つける必要がある。 本稿では、状態ベースと反例ベースのローカライゼーションという2つのパラダイムを比較して、検証対応言語の自動障害ローカライゼーションについて検討する。 我々の状態に基づくローカライゼーション戦略は、不審なプログラム状態を特定するために不変性を推論し、述示することでAutoFixの ‘snapshot' 方法論を再現する。 反例ベースの戦略は、生の反例抽出から構造化シングルトレースランキング、マルチトレースアグリゲーションに至るまで、検証者出力の使用を段階的に強化する一連の技術で構成されている。 これらの手法を検証するために,MutDafnyを用いて,DafnyBenchから多種多様な変異データセットを生成し,EXAMスコアを用いて局所化の有効性を評価する。 以上の結果から, 反例に基づくアプローチは, この設定における状態ベースローカライゼーションを著しく上回っていることがわかった。 単一トレース上の構造化されたランキングは、生の反例出力よりも最大の改善をもたらす一方、マルチトレースアグリゲーションは、ソルバによって導入されたパスバイアスを低減し、カバレッジを増大させることにより、ロバストネスとデバッギングユーティリティのさらなる向上をもたらす。 これらの結果から,検証対応言語における効果的なフォールトローカライゼーションは,逆例情報の利用と,その情報の構造化と多様化の方法の両方に依存することが明らかとなった。

関連論文リスト

• REVEAL: Reference-Grounded Reasoning for Multimodal Manipulation Detection [33.33464433821003]
  マルチモーダル操作検出は、偽画像のペアを同時に識別し、改ざんした領域をローカライズすることを目的としている。 人間の比較推論に触発されて、我々はこのタスクを基準基底検証問題として再検討する。 本稿では,この比較パラダイム用に明示的に設計されたフレームワークであるREVEALを提案する。
  論文  参考訳（メタデータ） (2026-05-27T13:24:41Z)
• Seeing the Needle in the Haystack: Towards Weakly-Supervised Log Instance Anomaly Localization via Counterfactual Perturbation [5.94150219760557]
  LogMILPは、バッグレベルの異常検出とインスタンスレベルの異常ローカライゼーションの両方を可能にする弱教師付きフレームワークである。 本手法は,プロトタイプ誘導構造モデルを用いてクリティカルログエントリをピンポイントする手法である。 3つの公開データセットの実験結果は、LogMILPが競合検出性能を達成することを示す。
  論文  参考訳（メタデータ） (2026-05-09T09:21:13Z)
• LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation [75.05397479715576]
  大規模言語モデル(LLM)とエージェントは有望な進歩を示しているが、その真の能力と失敗モードは未だ不明である。 CプログラムのためのLCMおよびエージェントベースの形式仕様生成に関する、最初の体系的および汚染に配慮した研究を提案する。
  論文  参考訳（メタデータ） (2026-05-02T11:31:33Z)
• ExVerus: Verus Proof Repair via Counterexample Reasoning [8.819482630789217]
  大規模言語モデル(LLM)のための逆例誘導フレームワークであるEXVERUSを提案する。 証明が失敗すると、EXVERUSは反例を自動生成して検証し、LSMを誘導して誘導不変量に一般化し、これらの障害を阻止する。 評価の結果,EXVERUSは最先端のプロンプトベースのVerus証明生成器よりも証明精度,堅牢性,トークン効率を著しく向上することがわかった。
  論文  参考訳（メタデータ） (2026-03-26T18:14:34Z)
• Dynamic analysis enhances issue resolution [53.50448142467294]
  DAIRA(Dynamic Analysis-enhanced Issue Resolution Agent)は、エージェントの推論サイクルに動的解析を組み込む自動修復フレームワークである。 テストトレース駆動の方法論によって駆動されるDAIRAは、軽量モニタを使用して重要なランタイムデータを抽出する。 Gemini 3 Flash Previewを使用すると、DAIRAは新たな最先端(SOTA)パフォーマンスを確立し、SWE-bench Verifiedデータセットで79.4%の解像度を達成する。
  論文  参考訳（メタデータ） (2026-03-23T14:48:54Z)
• Counterexample Guided Branching via Directional Relaxation Analysis in Complete Neural Network Verification [10.808953992870954]
  ディープニューラルネットワークは例外的な性能を示すが、敵の摂動に弱いままである。 現在のデータフローアプローチは、静的に依存するブラインドリファインメントプロセスで動作する。 本稿では,Falsification に積極的に寄与するニューロンの分岐を優先する Directional Gap を導入するフレームワーク DRG-BaB を提案する。
  論文  参考訳（メタデータ） (2026-03-16T04:57:44Z)
• Divide and Contrast: Source-free Domain Adaptation via Adaptive Contrastive Learning [122.62311703151215]
  Divide and Contrast (DaC) は、それぞれの制限を回避しつつ、両方の世界の善良な端を接続することを目的としている。 DaCは、ターゲットデータをソースライクなサンプルとターゲット固有なサンプルに分割する。 さらに、ソースライクなドメインと、メモリバンクベースの最大平均離散性(MMD)損失を用いて、ターゲット固有のサンプルとを整合させて、分散ミスマッチを低減する。
  論文  参考訳（メタデータ） (2022-11-12T09:21:49Z)
• Self-Supervised Training with Autoencoders for Visual Anomaly Detection [61.62861063776813]
  我々は, 正規サンプルの分布を低次元多様体で支持する異常検出において, 特定のユースケースに焦点を当てた。 我々は、訓練中に識別情報を活用する自己指導型学習体制に適応するが、通常の例のサブ多様体に焦点をあてる。 製造領域における視覚異常検出のための挑戦的なベンチマークであるMVTec ADデータセットで、最先端の新たな結果を達成する。
  論文  参考訳（メタデータ） (2022-06-23T14:16:30Z)

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

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