Counterexample-Based Fault Localization Outperforms State Methods in Verification Languages

Formal verification languages like Dafny embed correctness specifications directly into code, but when verification fails, developers struggle to pinpoint what went wrong. A new study from arXiv compares automated approaches to help developers trace errors back to their origin.

The Challenge with Verification Feedback#

When Dafny fails to verify code, it typically reports only the condition that failed—such as an unsatisfied postcondition—rather than where in the program logic the actual fault lies. While the tool can generate counterexamples that show concrete failing execution paths, developers must still manually sift through entire traces to locate the root cause.

Two Approaches to Fault Localization#

The research investigates two competing strategies:

• State-based localization: This method adapts AutoFix's "snapshot" technique by inferring invariants and identifying suspicious program states throughout execution.
• Counterexample-based localization: A family of methods that increasingly refine how verifier output is used—from extracting raw counterexamples, to ranking statements within a single trace, to aggregating patterns across multiple execution paths.

Key Findings#

The study evaluated these approaches using MutDafny to generate a dataset of mutated programs from DafnyBench, measuring success with the EXAM score. Results reveal that counterexample-based methods substantially outperformed state-based approaches. Within the counterexample family, structured ranking of statements within a single trace showed the largest improvement over basic output. Multi-trace aggregation added further gains by increasing coverage and reducing biases introduced by the solver's path selection.

Why It Matters#

The findings show that effective fault localization in verification languages depends not just on accessing counterexample data, but on how that data is organized and enriched. Diversifying across multiple execution paths helps eliminate misleading traces and gives developers a clearer picture of where bugs actually originate.