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

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. For example, in Dafny, while its counterexample features provide concrete execution traces, they typically expose a single failing path per assertion failure, leaving the developer to manually inspect 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 that uses MutDafny to generate a diverse mutant dataset from DafnyBench and measures 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 on how that information is structured and diversified.

Alexandra Mendes

Assistant Professor

My research focuses on encouraging a wider adoption of software verification by creating tools and methods that hide the complexities of verifying software. Much of my most recent work overlaps with the area of software engineering. For more details, see selected publications and some of my projects. Follow me on Twitter or add me on LinkedIn. See also the Software Reliability Lab website.