Improving Debugging in Verification-Aware Languages Through Automated Fault Localization: A Case Study in Dafny

• URL: http://arxiv.org/abs/2608.05399v2
• Date: Fri, 07 Aug 2026 14:31:04 GMT
• Title: Improving Debugging in Verification-Aware Languages Through Automated Fault Localization: A Case Study in Dafny
• Abstract summary: This paper investigates automated fault localization for verification-aware languages.<n>We compare two paradigms: state-based and counterexample-based localization.<n>Our results show that counterexample-based approaches substantially outperform state-based localization in this setting.
• Score: 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.

Related papers

• REVEAL: Reference-Grounded Reasoning for Multimodal Manipulation Detection [33.33464433821003]
  Multimodal manipulation detection aims to simultaneously identify forged image--text pairs and localize tampered regions.<n>Inspired by human comparative reasoning, we reformulate this task as a reference-grounded verification problem.<n>We propose REVEAL, a framework explicitly designed for this comparative paradigm.
  arXiv  Detail & Related papers  (2026-05-27T13:24:41Z)
• Seeing the Needle in the Haystack: Towards Weakly-Supervised Log Instance Anomaly Localization via Counterfactual Perturbation [5.94150219760557]
  LogMILP is a weakly supervised framework that enables both bag-level anomaly detection and instance-level anomaly localization.<n>Our method guides the model to pinpoint the critical log entries using prototype-guided structural modeling.<n> Experimental results on three public datasets demonstrate that LogMILP achieves competitive detection performance.
  arXiv  Detail & Related papers  (2026-05-09T09:21:13Z)
• LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation [75.05397479715576]
  Large language models (LLMs) and agents have shown promising progress, but their true capabilities and failure modes remain unclear.<n>We present the first systematic and contamination-aware study of LLM- and agent-based formal specification generation for C programs.
  arXiv  Detail & Related papers  (2026-05-02T11:31:33Z)
• Improving Dynamic Specification Inference with LLM-Generated Counterexamples [3.5558885788605332]
  This paper explores the use of large language models (LLMs) to automatically generate tests that attempt to invalidate generated assertions.<n>Our results show that state-of-the-art LLMs can generate effective counterexamples that help to discard up to 11.68% of invalid assertions inferred by SpecFuzzer.
  arXiv  Detail & Related papers  (2026-04-12T18:09:53Z)
• ExVerus: Verus Proof Repair via Counterexample Reasoning [8.819482630789217]
  We present EXVERUS, a counterexample-guided framework for large language models (LLMs)<n>When a proof fails, EXVERUS automatically generates and validates counterexamples, and then guides the LLM to generalize them into inductive invariants to block these failures.<n>Our evaluation shows that EXVERUS significantly improves proof accuracy, robustness, and token efficiency over the state-of-the-art prompting-based Verus proof generator.
  arXiv  Detail & Related papers  (2026-03-26T18:14:34Z)
• Dynamic analysis enhances issue resolution [53.50448142467294]
  DAIRA (Dynamic Analysis-enhanced Issue Resolution Agent) is an automated repair framework that embeds dynamic analysis into the agent's reasoning cycle.<n> Driven by a Test Tracing-Driven methodology, DAIRA utilizes lightweight monitors to extract critical runtime data.<n>When powered by Gemini 3 Flash Preview, DAIRA establishes a new state-of-the-art (SOTA) performance, achieving a 79.4% resolution rate on the SWE-bench Verified dataset.
  arXiv  Detail & Related papers  (2026-03-23T14:48:54Z)
• Counterexample Guided Branching via Directional Relaxation Analysis in Complete Neural Network Verification [10.808953992870954]
  Deep Neural Networks demonstrate exceptional performance but remain vulnerable to adversarial perturbations.<n>Current dataflow approaches operate with blind refinement processes that rely on statics.<n>We propose DRG-BaB, a framework that introduces the Directional Gap to prioritize branching on neurons actively contributing to falsification.
  arXiv  Detail & Related papers  (2026-03-16T04:57:44Z)
• CompassVerifier: A Unified and Robust Verifier for LLMs Evaluation and Outcome Reward [50.97588334916863]
  We develop CompassVerifier, an accurate and robust lightweight verifier model for evaluation and outcome reward.<n>It demonstrates multi-domain competency spanning math, knowledge, and diverse reasoning tasks, with the capability to process various answer types.<n>We introduce VerifierBench benchmark comprising model outputs collected from multiple data sources, augmented through manual analysis of metaerror patterns to enhance CompassVerifier.
  arXiv  Detail & Related papers  (2025-08-05T17:55:24Z)
• Divide and Contrast: Source-free Domain Adaptation via Adaptive Contrastive Learning [122.62311703151215]
  Divide and Contrast (DaC) aims to connect the good ends of both worlds while bypassing their limitations. DaC divides the target data into source-like and target-specific samples, where either group of samples is treated with tailored goals. We further align the source-like domain with the target-specific samples using a memory bank-based Maximum Mean Discrepancy (MMD) loss to reduce the distribution mismatch.
  arXiv  Detail & Related papers  (2022-11-12T09:21:49Z)
• Self-Supervised Training with Autoencoders for Visual Anomaly Detection [61.62861063776813]
  We focus on a specific use case in anomaly detection where the distribution of normal samples is supported by a lower-dimensional manifold. We adapt a self-supervised learning regime that exploits discriminative information during training but focuses on the submanifold of normal examples. We achieve a new state-of-the-art result on the MVTec AD dataset -- a challenging benchmark for visual anomaly detection in the manufacturing domain.
  arXiv  Detail & Related papers  (2022-06-23T14:16:30Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.