AI 中文总结
本文以 Dafny 为例，对比基于状态与基于反例的自动故障定位方法，通过 MutDafny 与 DafnyBench 开展评估，发现基于反例的方法更优，结构化排序与多轨迹聚合可提升定位效果。
AI 中文摘要
可验证感知语言（如 Dafny）将形式化规约直接集成到源代码中，以实现静态正确性检查。然而，当验证失败时，反馈通常仅限于错误的具体条件（如违反的后置条件），而非故障的根本原因。尽管 Dafny 的反例功能提供了具体的执行轨迹，但这些通常仅在每次断言失败时暴露一条失败路径，导致开发者需手动遍历整个轨迹以定位错误。本文研究可验证感知语言的自动故障定位，对比两种范式：基于状态的定位与基于反例的定位。我们的基于状态的定位策略复现 AutoFix 的“快照”方法，通过推断不变量和谓词来识别可疑程序状态。基于反例的策略包含一系列逐步丰富验证器输出使用方式的技术：从原始反例提取，到结构化单轨迹排序，再到多轨迹聚合。为验证这些方法，我们提出一个评估框架，使用 MutDafny 从 DafnyBench 生成多样化的变异体数据集，并通过 EXAM 分数衡量定位有效性。结果表明，在该场景下，基于反例的方法显著优于基于状态的定位；对单轨迹的结构化排序相比原始反例输出带来最大提升，而多轨迹聚合通过增加覆盖率、减少求解器引入的路径偏差，进一步提升了鲁棒性和调试实用性。这些发现表明，可验证感知语言中的有效故障定位既依赖于反例信息，也依赖于该信息的结构化与多样化方式。
英文摘要
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.
