Pith. sign in

REVIEW 3 major objections 6 minor 36 references

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

T0 review · 3 major / 6 minor · reviewed 2026-08-10 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read Automated fault localization for Dafny works far better when it ranks many verifier counterexample paths instead of inferring suspicious program states.

desk verdict Solid empirical comparison showing counterexample-based localization beats state-based in Dafny, but the multi-trace method's exhaustiveness claim is overreached and needs a fix before this is fully convincing. read the letter →

arxiv 2608.05399 v2 pith:RUN4AXRH submitted 2026-08-05 cs.SE

Álvaro Silva , Isabel Amaral , João Pascoal Faria , Alexandra Mendes This is my paper · ORCID
classification cs.SE
keywords faultlocalizationDafnycounterexamplesverification-awarelanguagesdesignbycontractmutationtestingEXAMscoremulti-traceaggregation
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

When a Dafny program fails verification, the verifier reports a violated condition and usually one representative counterexample trace, but not which line caused the failure. This paper tries to establish that fault localization for such verification-aware languages is more effective when it treats those counterexample traces as first-class evidence and aggregates several of them, rather than reconstructing suspicious program states from test runs. It builds a state-based ranker (SNAP) that adapts the AutoFix snapshot methodology to Dafny, and a counterexample-based family (CNTB, CNTS, CNTM) that moves from raw trace extraction to structured ranking to multi-trace aggregation via iterative path blocking. Across 500 Dafny mutants, the paper reports that the multi-trace counterexample ranker requires inspecting far fewer lines on average, finds the fault in many more programs, and ranks it top-1 far more often than the state-based approach. If this holds, developers debugging verification failures can receive a ranked list of lines that points near the root cause instead of a single arbitrary failing path.

What carries the argument

The central object is the aggregate path set, a collection of independent counterexample execution paths for one failing verification condition. It is produced by iterative path blocking: each round inserts `assume false` at the deepest branch point of the latest counterexample so the SMT solver is pushed toward a different failing path, and the loop stops when no new counterexample appears. Lines are then ranked lexicographically by four components: frequency across the collected paths, maximum nesting depth, whether the line is a control-statement guard, and trace order. That rank tuple is what turns raw solver output into a developer-facing list of likely fault locations.

What would settle it

Take a program with two distinct verification failures that enter the same deepest branch but diverge after that branch point; run CNTM's iterative path blocking and check whether both failing paths appear in the collected path set. If the later-diverging path is pruned and missing, the claim that the loop captures all unique failing paths is false.

Watch

Extended reading notes

Core claim

The paper's central claim is that in a verification-aware language like Dafny, counterexample-based fault localization outperforms state-based localization, and that the way counterexample information is structured and diversified matters as much as its existence. The primary technique, CNTM, repeatedly runs the verifier and, after each counterexample, inserts an `assume false` statement at the deepest branch point of the discovered path, forcing the solver to find a different failing path; it then ranks every line appearing in the collected paths by frequency, nesting depth, control-statement status, and trace order. On 500 mutants built from DafnyBench with MutDafny, the paper reports that a developer inspects about one third as many lines on average (file-scope EXAM of 0.109 versus 0.324), that the correct line is ranked first in 43% of cases versus 8%, and that the fault appears somewhere in the ranking in 84% of cases versus 47%. The ablation shows that removing structural context roughly doubles the inspection effort, and that dropping the depth heuristic is the most damaging single change; an unoptimized large-language-model (LLM) baseline achieves higher Top-1 accuracy (58%) but worse average inspection effort and found rate, which the paper reads as complementary strengths rather than a direct competition.

Load-bearing premise

The method assumes that inserting `assume false` at the deepest branch point of a discovered counterexample prunes exactly that path class and leaves every other failing path reachable, so the loop stops only when all distinct failing paths have been captured.

Editorial extensions

If this is right

  • Developers debugging Dafny verification failures can expect to inspect about one third as many lines when the ranking aggregates multiple counterexample paths instead of relying on one trace.
  • Structural features of the code, especially nesting depth, are a major driver of localization quality; raw counterexample lines without control-flow context are close to twice as costly to search.
  • Multi-trace aggregation improves robustness by raising the found rate to 84% and cutting empty outputs to 1.4%, meaning fewer cases where the developer gets no useful lead.
  • LLM ranking and counterexample ranking have complementary strengths: an LLM is better at putting the faulty line first, while the counterexample ranker gives better overall ranking quality and higher coverage.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The termination claim that the loop has 'captured all unique failing paths' may be too strong: blocking the deepest branch point prunes every path that shares that branch decision but diverges later, so two distinct failures that branch at the same point will be conflated and one can be missed.
  • Because the dataset comes from DafnyBench's pedagogical and algorithmic programs, the reported gap could shrink on industrial verification code with longer functions, messier control flow, or specification faults rather than implementation-only faults.
  • The observed LLM Top-1 advantage suggests a concrete hybrid that the paper leaves untested: use CNTM to select a small candidate region, then let an LLM pick the single most suspicious line in that region and measure whether Top-1 and EXAM both improve.
  • The same multi-trace aggregation idea could be evaluated in other contract-based languages (for instance Verus) where the verifier also emits one counterexample per failure; the key precondition is that the trace exposes branch structure clearly enough to instrument.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 6 minor

Summary. This paper compares two fault-localization paradigms for Dafny: a state-based approach (SNAP) adapted from AutoFix, and a family of counterexample-based techniques (CNTB, CNTS, CNTM) that increasingly exploit verifier output. The evaluation is carried out on 500 mutants sampled from DafnyBench and generated with MutDafny, using EXAM, Top-k, Found-rate, and Empty-rate metrics under both file and method scope. The authors report that CNTM substantially outperforms SNAP (file-scope EXAM 0.109 vs. 0.324, Top-1 43% vs. 8%), that structured ranking yields the main improvement over raw counterexample extraction, and that multi-trace aggregation adds further gains (CNTM vs. CNTS Top-1 43% vs. 27%). An LLM baseline is included for context, showing complementary strengths.

Significance. If the central empirical conclusions hold, this paper provides a valuable benchmark and baseline for fault localization in verification-aware languages, a relatively underexplored setting. The study is careful in several respects: the random sampling of 500 mutants from a larger pool is justified with existing sample-size guidelines; paired Wilcoxon and McNemar tests with effect sizes are reported; an ablation study isolates ranking components; and a complete-output subset analysis partially addresses the weakness of the SNAP baseline. The paper also ships concrete artifacts (DAFNYCBT, the Dafny frontend for Daikon, and the counterexample tooling) and makes the reproduction package available. The main weakness is the claim that CNTM's iterative blocking exhaustively collects all unique failing paths; this claim is not established by the described instrumentation and is load-bearing for RQ3.

major comments (3)
  1. [Section VI-C (RQ3) and Table IV] The termination claim in Step 5 that 'no further counterexamples are generated, indicating all unique failing paths have been captured' does not follow from the instrumentation described in Step 3. Injecting 'assume false' at the deepest branch point of the current counterexample prunes every failing path that shares that branch decision and diverges later, not just the discovered path. Thus the aggregate path set Π can be incomplete, and the frequency feature freq(l) in the ranking tuple of Section III-F is computed over a potentially biased sample of failing paths. The Listing 1 example is a special case in which each failing path occupies a distinct top-level branch, so it does not demonstrate exhaustiveness in general. This matters because RQ3's claim that multi-trace aggregation improves robustness 'by increasing coverage and reducing path bias' rests on the completeness of Π. Please either weaken the claim to say that more paths are collected rather than all paths, or add evidence that the blocking strategy is complete (e.g., by blocking full path conditions, or by comparing against exhaustive enumeration on small programs).
  2. [Section VI-C (RQ3) and Table IV] The reported gains of CNTM over CNTS (file EXAM 0.127 to 0.109; Top-1 27% to 43%) are attributed to multi-trace aggregation, but the design does not isolate the effect of the specific deepest-branch blocking heuristic from the simple act of collecting more counterexamples. Given the incompleteness concern above, the improvement could also arise from the extra verifier re-runs or from a pruning order that happens to favor the mutated line. The paper should either add an ablation that aggregates multiple raw counterexamples without the deepest-branch blocking, or explicitly acknowledge this alternative explanation in the RQ3 discussion.
  3. [Section V-A (Experimental Procedure) and Section VI-A (RQ1)] SNAP is evaluated with DAFNYCBT, an early prototype that produces valid tests for only 387 of the 500 programs, and SNAP's high Empty rate (39.20%) is largely attributed to this tool. The authors do provide a 297-program complete-output subset, and the gap persists there (file EXAM 0.212 vs. 0.092), which is reassuring. However, the representativeness of these 297 programs relative to the full 500 is not reported; if the subset is skewed toward simpler contracts or certain mutation operators, the strength of the RQ1 conclusion would change. Please report the mutation-operator and program-complexity distribution of the subset, or justify why the subset comparison is sufficient for the broad claim that counterexample-based approaches are 'substantially' better in this setting.
minor comments (6)
  1. [Tables IV and V] Several table headers contain typos ('PROGRAMNS', 'DEFINES INII', 'AS DEFINED INTABLEII'); please correct them for consistency with Table II.
  2. [References] Reference [13] lists an author as 'P. M.' with an apparently missing surname; please complete the author list.
  3. [Section VI-A (RQ1)] The derivation of RAND's expected file-scope EXAM appears to be off by a factor of about two: if RAND lists the methods lines in uniformly random order, the expected number of non-fault lines before the faulty one is roughly (m-1)/2, giving an EXAM of about (m-1)/(2(N-1)), i.e., about half the method-to-file size ratio, not the ratio itself. Please clarify the calculation or replace the explanatory text with the measured value.
  4. [Abstract and Section VI-C] The phrase 'reducing path bias introduced by the solver' is not directly measured anywhere in the evaluation; consider softening it or adding a quantitative indicator of path diversity (e.g., number of paths collected per program).
  5. [Section VI-A (RQ1)] There is a typo in 'When paths containing fauls are insufficiently covered'; 'fauls' should be 'faults'.
  6. [Section III-A] Calling SNAP a 'dynamic analysis technique' is clear in context, but since Dafny is statically verified, 'test-execution-based' might avoid confusion with Dafny's own dynamic frames or ghost state terminology.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity; CNTM's ranking chain is self-contained, and the path-blocking exhaustiveness concern is a validity issue, not a circular reduction.

full rationale

The claimed derivation chain is self-contained. CNTM's ranking tuple is built directly from verifier counterexample paths and source-level structure (frequency, max depth, control-statement flag, trace order); no parameter is fitted to the EXAM scores the technique is later measured against, and the CNTB/CNTS ablations are genuine comparisons rather than predictions forced by construction. External anchors (RAND and an LLM baseline) ground the evaluation, and SNAP adopts AutoFix's externally published alpha/beta/gamma values rather than values fit in this paper. The use of MutDafny, a mutation tool by two of the present authors, to generate the benchmark is a self-citation, but it is not load-bearing: the ground truth is an independent diff against the external DafnyBench programs, the localization ranking does not depend on MutDafny's operator definitions, and the artifact is made available for reproduction. The potential weakness in Section III-E, where inserting 'assume false' at the deepest branch point prunes every failing path sharing that branch and termination therefore does not guarantee that 'all unique failing paths have been captured', is an unsupported exhaustiveness claim and a robustness threat to validity, not a circular equation or a fitted-input-renamed-as-prediction. It does not make CNTM's output equivalent to its inputs or to any self-cited result.

Assumptions & free parameters 1 free parameters · 5 assumptions · 0 invented entities

The central claim (CNTM outperforms SNAP) does not depend on any numeric parameter fitted to the benchmark. The only free parameter listed belongs to the inherited AutoFix suspiciousness formula for SNAP. The axioms are domain assumptions about the benchmark, the verifier's diagnostics, and the path-blocking mechanism. No new ontological entities are proposed.

free parameters (1)
  • SNAP suspiciousness weights alpha, beta, gamma = alpha=1/3, beta=2/3, gamma=1
    Adopted from AutoFix's empirically determined values (Section II-D) and applied to SNAP's dynamic score. They are not fitted to the Dafny dataset and do not feed into the proposed CNTM technique, so they do not affect the central claim.
assumptions (5)
  • domain assumption A Dafny program that fails verification contains an implementation fault (not a specification fault), and the mutated line from the diff is the ground-truth fault location.
    Stated in Section I as a formalization for controlled evaluation. It excludes specification errors, which are common in real debugging, and makes the mutant diff the ground truth.
  • domain assumption Dafny's counterexample diagnostics faithfully report the ordered source lines of a failing execution path.
    CNTB, CNTS, and CNTM consume Dafny CLI counterexample traces directly (Section III-A). If the traces are partial, symbolic, or omit loop iterations, the resulting rankings inherit those distortions.
  • ad hoc to paper Injecting 'assume false' at the deepest branch point of a discovered path prunes exactly the discovered path class and preserves all other failing paths.
    This is the core mechanism of CNTM (Section III-E, Steps 2-4). The paper asserts that it prunes 'the discovered path' and terminates when 'all unique failing paths have been captured', but no proof is given. Paths that share the branch decision but diverge later are also pruned, so the enumeration is not exhaustive.
  • domain assumption Daikon's likely invariants inferred from instrumented print traces correctly represent passing and failing program states for SNAP.
    SNAP's snapshot generation (Section II-C) depends on a custom frontend that converts print statements into Daikon trace files. Any missing variable values or trace corruption would alter the passing/failing invariant sets and the resulting ranking.
  • domain assumption MutDafny's mutation operators produce faults representative of real Dafny bugs.
    The evaluation's external validity rests on the claim that the mutated faults resemble real Dafny bugs (Section VII). The operators were designed using GitHub bugfix evidence, but the dataset itself contains only synthetic mutations.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Improving Debugging in Verification-Aware Languages Through Automated Fault Localization: A Case Study in Dafny." pith.science (2026). https://pith.science/paper/RUN4AXRH

@misc{pith2026260805399,
  author       = {Pith},
  title        = {Pith review of: Improving Debugging in Verification-Aware Languages Through Automated Fault Localization: A Case Study in Dafny},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/RUN4AXRH}},
  note         = {Machine review of arXiv:2608.05399}
}
read the original 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.

Figures

Figures reproduced from arXiv: 2608.05399 by the authors.

Figure 1
Figure 1. Distribution of file-scoped EXAM scores. The boxplots illustrate [PITH_FULL_IMAGE:figures/full_fig_p009_1.png] view at source ↗

Review history (2 revisions) →

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

36 extracted references · 2 linked inside Pith

  1. [1]

    Dafny: An automatic program verifier for functional correctness,

    K. R. M. Leino, “Dafny: An automatic program verifier for functional correctness,” inLogic for Programming, Artificial Intelligence, and Reasoning(E. M. Clarke and A. V oronkov, eds.), (Berlin, Heidelberg), pp. 348–370, Springer Berlin Heidelberg, 2010

    2010

  2. [2]

    Verus: Verifying rust programs using linear ghost types,

    A. Lattuada, T. Hance, C. Cho, M. Brun, I. Subasinghe, Y . Zhou, J. Howell, B. Parno, and C. Hawblitzel, “Verus: Verifying rust programs using linear ghost types,”Proceedings of the ACM on Programming Languages, vol. 7, no. OOPSLA1, pp. 286–315, 2023

    2023

  3. [3]

    Automated fixing of programs with contracts,

    Y . Pei, C. A. Furia, M. Nordio, Y . Wei, B. Meyer, and A. Zeller, “Automated fixing of programs with contracts,”IEEE Transactions on Software Engineering, vol. 40, no. 5, pp. 427–449, 2014

    2014

  4. [4]

    Eiffel: A language and environment for software engineer- ing,

    B. Meyer, “Eiffel: A language and environment for software engineer- ing,”Journal of Systems and Software, vol. 8, no. 3, pp. 199–246, 1988

    1988

  5. [5]

    Dafnybench: A benchmark for formal software verification,

    C. Loughridge, Q. Sun, S. Ahrenbach, F. Cassano, C. Sun, Y . Sheng, A. Mudide, M. R. H. Misu, N. Amin, and M. Tegmark, “Dafnybench: A benchmark for formal software verification,”arXiv preprint arXidafny- benchv:2406.08467, 2024

    arXiv 2024

  6. [6]

    Mutdafny: A mutation-based approach to assess dafny specifications,

    I. Amaral, A. Mendes, and J. Campos, “Mutdafny: A mutation-based approach to assess dafny specifications,” in2026 IEEE/ACM 48th International Conference on Software Engineering (ICSE), 2026

    2026

  7. [7]

    Using test oracles generated from program documentation,

    D. Peters and D. Parnas, “Using test oracles generated from program documentation,”IEEE Transactions on Software Engineering, vol. 24, no. 3, pp. 161–173, 1998

    1998

  8. [8]

    A simple and practical approach to unit testing: The jml and junit way,

    Y . Cheon and G. T. Leavens, “A simple and practical approach to unit testing: The jml and junit way,” inProceedings of the 16th European Conference on Object-Oriented Programming, ECOOP ’02, (Berlin, Heidelberg), p. 231–255, Springer-Verlag, 2002

    2002

Show all 36 references
  1. [9]

    Approaches to specification- based testing,

    D. Richardson, O. O’Malley, and C. Tittle, “Approaches to specification- based testing,”SIGSOFT Softw. Eng. Notes, vol. 14, p. 86–96, Nov. 1989

    1989

  2. [10]

    Specification based testing: Towards practice,

    A. K. Petrenko, “Specification based testing: Towards practice,” in Perspectives of System Informatics(D. Bjørner, M. Broy, and A. V . Zamulin, eds.), (Berlin, Heidelberg), pp. 287–300, Springer Berlin Heidelberg, 2001

    2001

  3. [11]

    Programs that test themselves,

    B. Meyer, A. Fiva, I. Ciupa, A. Leitner, y. Wei, and E. Stapf, “Programs that test themselves,”Computer, vol. 42, pp. 46 – 55, 10 2009

    2009

  4. [12]

    Delfy: Dynamic test generation for dafny,

    P. Spettel, “Delfy: Dynamic test generation for dafny,” Master’s thesis, Eidgen¨ossische Technische Hochschule Z ¨urich, 2013

    2013

  5. [13]

    Integrated en- vironment for diagnosing verification errors,

    M. Christakis, R. Leino, P. M. , and V . W ¨ustholz, “Integrated en- vironment for diagnosing verification errors,” in22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’16), pp. 424–441, Springer, April 2016

    2016

  6. [14]

    A toolkit for automated testing of dafny,

    A. Fedchin, T. Dean, J. S. Foster, E. Mercer, Z. Rakamari ´c, G. Reger, N. Rungta, R. Salkeld, L. Wagner, and C. Waldrip, “A toolkit for automated testing of dafny,” inNASA Formal Methods: 15th Interna- tional Symposium, NFM 2023, Houston, TX, USA, May 16–18, 2023, Proceedings...

    2023

  7. [15]

    The daikon system for dynamic detection of likely invariants,

    M. D. Ernst, J. H. Perkins, P. J. Guo, S. McCamant, C. Pacheco, M. S. Tschantz, and C. Xiao, “The daikon system for dynamic detection of likely invariants,”Science of Computer Programming, vol. 69, no. 1, pp. 35–45, 2007. Special issue on Experimental Software and Toolkits

    2007

  8. [16]

    Automated fault localization using potential invariants,

    B. Pytlik, M. Renieris, S. Krishnamurthi, and S. P. Reiss, “Automated fault localization using potential invariants,” inAADEBUG 2003: Fifth International Workshop on Automated and Algorithmic Debugging, (Ghent, Belgium), pp. 273–276, Sept. 2003

    2003

  9. [17]

    Visualization of test information to assist fault localization,

    J. Jones, M. Harrold, and J. Stasko, “Visualization of test information to assist fault localization,” inProceedings of the 24th International Conference on Software Engineering. ICSE 2002, pp. 467–477, 2002

    2002

  10. [18]

    An evaluation of sim- ilarity coefficients for software fault localization,

    R. Abreu, P. Zoeteweij, and A. J. Van Gemund, “An evaluation of sim- ilarity coefficients for software fault localization,” in2006 12th Pacific Rim International Symposium on Dependable Computing (PRDC’06), pp. 39–46, 2006

    2006

  11. [19]

    The dstar method for effective software fault localization,

    W. E. Wong, V . Debroy, R. Gao, and Y . Li, “The dstar method for effective software fault localization,”IEEE Transactions on Reliability, vol. 63, no. 1, pp. 290–308, 2014

    2014

  12. [20]

    On the accuracy of spectrum-based fault localization,

    R. Abreu, P. Zoeteweij, and A. J. van Gemund, “On the accuracy of spectrum-based fault localization,” inTesting: Academic and In- dustrial Conference Practice and Research Techniques - MUTATION (TAICPART-MUTATION 2007), pp. 89–98, 2007

    2007

  13. [21]

    Qwen3-coder-next technical report,

    R. Cao, M. Chen, J. Chen, Z. Cui, Y . Feng, B. Hui, Y . Jing, K. Li, M. Li, J. Lin,et al., “Qwen3-coder-next technical report,”arXiv preprint arXiv:2603.00729, 2026

    2026 arXiv

  14. [22]

    How hard does mutation analysis have to be, anyway?,

    R. Gopinath, A. Alipour, I. Ahmed, C. Jensen, and A. Groce, “How hard does mutation analysis have to be, anyway?,” in2015 IEEE 26th International Symposium on Software Reliability Engineering (ISSRE), pp. 216–227, IEEE, 2015

    2015

  15. [23]

    Threats to the validity and value of empirical assessments of the accuracy of coverage-based fault locators,

    F. Steimann, M. Frenkel, and R. Abreu, “Threats to the validity and value of empirical assessments of the accuracy of coverage-based fault locators,” inProceedings of the 2013 International Symposium on Software Testing and Analysis, pp. 314–324, 2013

    2013

  16. [24]

    Evaluating and improving fault localization,

    S. Pearson, J. Campos, R. Just, G. Fraser, R. Abreu, M. D. Ernst, D. Pang, and B. Keller, “Evaluating and improving fault localization,” in2017 IEEE/ACM 39th International Conference on Software Engi- neering (ICSE), pp. 609–620, IEEE, 2017

    2017

  17. [25]

    Laurel: Unblocking automated verification with large language mod- els,

    E. Mugnier, E. A. Gonzalez, N. Polikarpova, R. Jhala, and Z. Yuanyuan, “Laurel: Unblocking automated verification with large language mod- els,”Proceedings of the ACM on Programming Languages, vol. 9, no. OOPSLA1, pp. 1519–1545, 2025

    2025

  18. [26]

    Test case purification for improving fault localization,

    J. Xuan and M. Monperrus, “Test case purification for improving fault localization,” inProceedings of the 22nd ACM SIGSOFT international symposium on foundations of software engineering, pp. 52–63, 2014

    2014

  19. [27]

    Mure: making use of mutations to refine spectrum-based fault localization,

    Z. Li, L. Yan, Y . Liu, Z. Zhang, and B. Jiang, “Mure: making use of mutations to refine spectrum-based fault localization,” in2018 IEEE International Conference on Software Quality, Reliability and Security Companion (QRS-C), pp. 56–63, IEEE, 2018

    2018

  20. [28]

    Empirical evaluation of the tarantula automatic fault-localization technique,

    J. A. Jones and M. J. Harrold, “Empirical evaluation of the tarantula automatic fault-localization technique,” inProceedings of the 20th IEEE/ACM International Conference on Automated Software Engineer- ing, ASE ’05, (New York, NY , USA), p. 273–282, Association for Computing ...

    2005

  21. [29]

    Spectrum-based multi- ple fault localization,

    R. Abreu, P. Zoeteweij, and A. J. van Gemund, “Spectrum-based multi- ple fault localization,” in2009 IEEE/ACM International Conference on Automated Software Engineering, pp. 88–99, 2009

    2009

  22. [30]

    Ask the mutants: Mutating faulty programs for fault localization,

    S. Moon, Y . Kim, M. Kim, and S. Yoo, “Ask the mutants: Mutating faulty programs for fault localization,” in2014 IEEE Seventh Inter- national Conference on Software Testing, Verification and Validation, pp. 153–162, 2014

    2014

  23. [31]

    Metallaxis-fl: mutation-based fault localization,

    M. Papadakis and Y . Le Traon, “Metallaxis-fl: mutation-based fault localization,”Software Testing, Verification and Reliability, vol. 25, p. 605–628, Aug. 2015

    2015

  24. [32]

    Automatic program repair using formal verification and expression templates,

    T.-T. Nguyen, Q.-T. Ta, and W.-N. Chin, “Automatic program repair using formal verification and expression templates,” inVerification, Model Checking, and Abstract Interpretation(C. Enea and R. Piskac, eds.), (Cham), pp. 70–91, Springer International Publishing, 2019

    2019

  25. [33]

    Specification-guided repair of arithmetic errors in dafny programs using LLMs,

    V . Wu, A. Mendes, and A. Abreu, “Specification-guided repair of arithmetic errors in dafny programs using LLMs,” inSoftware Engi- neering and Formal Methods: 23rd International Conference, SEFM 2025, Toledo, Spain, November 10–14, 2025, Proceedings, (Berlin, Heidelberg), p. 2...

    2025

  26. [34]

    Automated test generation and mutation testing for alloy,

    A. Sullivan, K. Wang, R. N. Zaeem, and S. Khurshid, “Automated test generation and mutation testing for alloy,” in2017 IEEE International Conference on Software Testing, Verification and Validation (ICST), pp. 264–275, IEEE, 2017

    2017

  27. [35]

    Flack: Counterexample-guided fault localization for alloy models,

    G. Zheng, T. Nguyen, S. G. Brida, G. Regis, M. F. Frias, N. Aguirre, and H. Bagheri, “Flack: Counterexample-guided fault localization for alloy models,” in2021 IEEE/ACM 43rd International Conference on Software Engineering (ICSE), pp. 637–648, IEEE, 2021

    2021

  28. [36]

    Fault localization on verification witnesses,

    D. Beyer, M. Kettl, and T. Lemberger, “Fault localization on verification witnesses,” inInternational Symposium on Model Checking Software, pp. 205–224, Springer, 2024

    2024

Pith tools

Reviewed August 10, 2026 · model on record in the stance chip above.