{"id":"a2160f7b-1cba-451d-adde-a0d6cf1efdd5","arxiv_id":"2608.05399","paper_version":2,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":1,"one_line_summary":"Counterexample-based multi-trace fault localization (CNTM) substantially outperforms state-based snapshot ranking for Dafny, with file-scope EXAM 0.109 vs 0.324.","lead":"This paper shows that for Dafny, a language with built-in formal specifications, debugging is faster when you mine the verifier's counterexample traces instead of summarizing program states. The best method gathers many failing paths, ranks lines by how often and how deeply they appear, and cuts the average search effort for finding a bug.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The weakest point is CNTM's claimed exhaustive path enumeration: §III-E blocks the deepest branch point with 'assume false', which prunes every failing path sharing that branch, so the path set need not contain all unique failing paths and the path-diversity claim is not established.","rationale":"The reader's weakest assumption identifies the same load-bearing concern: the path-blocking step does not guarantee that all unique failing paths are captured. I agree with that diagnosis, and the manuscript itself contains the unsupported assertion in §III-E that termination implies exhaustiveness. However, I do not think this warrants changing the reader's conditional verdict. The primary empirical claim, that counterexample-based localization substantially outperforms the state-based SNAP baseline, is supported by the full-dataset results (EXAM 0.109 vs 0.324) and, importantly, by the subset of 297 programs where all methods produce non-empty outputs (EXAM 0.092 vs 0.212). The path-exhaustiveness issue mainly affects the interpretation of RQ3 and the robustness attribution in the abstract, not the existence of a substantial gap between paradigms. The paper also deserves credit for including paired statistical tests, an ablation study, and a subset analysis that addresses the most obvious confound in the SNAP comparison. The conditional accept remains appropriate: the authors should soften the 'all unique failing paths' wording, provide per-mutant trace counts to show how often more than one path is actually collected, and release artifacts so the exact path-blocking variant can be checked. If the exact variant were to show that CNTM's advantage over CNTS disappears, then the central diversity claim would need to be reconsidered; that is precisely why the proposed test is the right settling check.","tokens_in":19265,"tokens_out":6475,"duration_ms":77581,"concrete_test":"Re-run CNTM on the same 500 mutants with an exact path-blocking variant: instead of injecting 'assume false' at the deepest branch point, block the entire discovered path by conjoining all branch decisions along that counterexample trace (or by adding a solver-level path constraint), then compare EXAM, Top-1, Found rate, and the number of traces collected per mutant against the published deepest-branch version. If the exact variant collects strictly more traces and changes results materially, the completeness overclaim has empirical bite and the reported path-diversity gains are not attributable to genuine path coverage; if the results are equivalent, the deepest-branch heuristic may be adequate even though its stated termination criterion is technically unsound.","verdict_should_be":"UNCHANGED","load_bearing_attack":"CNTM's central methodological novelty is multi-trace aggregation, and its justification rests on §III-E's claim that iterative path blocking terminates 'indicating all unique failing paths have been captured.' The actual instrumentation inserts 'assume false' at the deepest branch point of the current counterexample. That blocks not just the discovered path but every failing path that enters the same branch and diverges later, so the termination condition 'no further counterexamples are generated' is not sufficient for exhaustiveness. Consequently, the frequency feature freq(l) in the ranking tuple (§III-F) is computed over an incomplete and potentially biased path set. The paper reports that CNTM improves over CNTS (EXAM 0.109 vs 0.127, Top-1 43% vs 27%), but does not establish that this gain comes from true path diversity rather than from the extra verifier re-runs or from pruning paths in a way that happens to favor the mutated line. This does not destroy the central head-to-head comparison against SNAP, which still holds on the 297-program complete-output subset, but it does undercut the specific RQ3 claim that multi-trace aggregation improves robustness by increasing coverage and reducing path bias. The overclaim is explicit, located in §III-E and the abstract, and should be corrected or empirically supported.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":19495,"tokens_out":7115,"duration_ms":73068,"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":[{"comment":"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).","section":"Section VI-C (RQ3) and Table IV"},{"comment":"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.","section":"Section VI-C (RQ3) and Table IV"},{"comment":"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.","section":"Section V-A (Experimental Procedure) and Section VI-A (RQ1)"}],"minor_comments":[{"comment":"Several table headers contain typos ('PROGRAMNS', 'DEFINES INII', 'AS DEFINED INTABLEII'); please correct them for consistency with Table II.","section":"Tables IV and V"},{"comment":"Reference [13] lists an author as 'P. M.' with an apparently missing surname; please complete the author list.","section":"References"},{"comment":"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.","section":"Section VI-A (RQ1)"},{"comment":"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).","section":"Abstract and Section VI-C"},{"comment":"There is a typo in 'When paths containing fauls are insufficiently covered'; 'fauls' should be 'faults'.","section":"Section VI-A (RQ1)"},{"comment":"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.","section":"Section III-A"}],"recommendation":"major_revision","confidential_remarks":"The paper is a solid empirical study with honest threats-to-validity and reproducible artifacts. The main issue is the overclaim about exhaustive path collection in CNTM; I believe this is fixable within the scope of the paper by weakening the claim or adding supporting evidence. The central head-to-head comparison against SNAP is defensible even if the path-diversity mechanism is not fully established. I do not see evidence of deliberate overstatement, and the self-reliance on MutDafny and DAFNYCBT is a natural but acknowledged limitation that could be addressed with a short subset-representativeness analysis."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Here's the short version: the central comparison is likely right—counterexample-based localization beats a state-based AutoFix-style approach on Dafny mutants—and the main new idea, CNTM, is worth taking seriously. But the paper overclaims that its iterative path blocking exhaustively enumerates all failing paths, and that specific claim needs to be fixed or supported before publication.\n\nWhat is actually new: CNTM, which injects 'assume false' at the deepest branch point of each counterexample to force the solver to find other failing paths, then ranks lines by frequency across those paths, nesting depth, and control-node status. There is also DAFNYCBT, a contract-based test generator needed to run the SNAP baseline. And there is a clean experimental framework: 500 mutants from DafnyBench, paired Wilcoxon/McNemar tests, an ablation, and a subset analysis that strips out SNAP's empty outputs. The result that CNTM achieves EXAM 0.109 vs 0.324 for SNAP, with Top-1 43% vs 8%, is internally consistent and survives the subset analysis (EXAM 0.092 vs 0.212). The ablation shows structural depth matters most; frequency and control nodes help mainly for Top-1. That is a believable, well-executed empirical study.\n\nThe soft spot is the exhaustiveness claim in Section III-E. Step 5 says the loop terminates when no further counterexamples are generated, 'indicating all unique failing paths have been captured.' That is not justified. Blocking the deepest branch point with assume false prunes every path that goes through that branch, not just the one the solver found, so the collected path set need not include all distinct failing classes. The frequency feature is then computed over a possibly incomplete and biased set. This does not sink the SNAP comparison, which is robust to it, but it does undercut the RQ3 claim that multi-trace aggregation improves robustness by 'reducing path bias.' The improvement over single-trace CNTS could come partly from extra verifier re-runs or from pruning that happens to favor the mutated line. The authors should either soften the language to 'a set of diverse paths' or empirically demonstrate coverage, e.g., by comparing against exhaustive enumeration on small programs or by measuring the number of paths found vs known failing branches.\n\nOther notes: the benchmark uses the authors' own MutDafny and DAFNYCBT, a self-reliance concern but not fatal—they cite MutDafny as prior work and mutation-based evaluation is standard. A per-operator breakdown would strengthen confidence that results are not driven by a few operator types. The code and data are promised only after acceptance; for a paper whose main evidence is empirical, they should be released with the submission.\n\nWho this is for: researchers working on fault localization for Dafny or verification-aware languages, and anyone designing verifier-native debugging tools. It deserves a serious referee; the main result is probably correct, but the path-enumeration claim needs correction and the artifacts should be public. I'd accept it conditionally, not desk-reject, and would ask for those revisions.","headline":"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.","tokens_in":20075,"tokens_out":3015,"would_cite":true,"duration_ms":29886,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"Automated fault localization for Dafny works far better when it ranks many verifier counterexample paths instead of inferring suspicious program states.","keywords":["fault localization","Dafny","counterexamples","verification-aware languages","design by contract","mutation testing","EXAM score","multi-trace aggregation"],"falsifier":"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.","tokens_in":18996,"feed_emoji":"🐛","tokens_out":13237,"duration_ms":111353,"temperature":0.7,"pith_summary":"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.","feed_headline":"Diverse counterexample paths cut Dafny fault search by two-thirds","feed_subtitle":"Ranking multiple verifier counterexample paths beats state-snapshot inference on 500 Dafny mutants.","key_machinery":"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.","core_discovery":"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.","pith_inferences":["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."],"forward_implications":["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."],"supporting_citations":[{"why":"Defines Dafny and its automatic verification of functional correctness, the language setting the whole study targets.","marker":"[1]"},{"why":"Supplies the AutoFix snapshot methodology that SNAP replicates as the state-based comparison paradigm.","marker":"[3]"},{"why":"Provides the DafnyBench program collection from which the 500-mutant evaluation dataset is derived.","marker":"[5]"},{"why":"Contributes the MutDafny mutation operators used to generate the faulty programs that serve as ground truth.","marker":"[6]"},{"why":"Daikon is the dynamic invariant inference engine SNAP relies on to build passing and failing snapshots.","marker":"[15]"},{"why":"Defines the EXAM metric and the convention for estimating remaining search effort when the faulty line is absent from a ranking.","marker":"[24]"}],"fun_headline_variants":["Counterexample ranking cuts Dafny fault search by two-thirds","Structured counterexample paths beat state snapshots in Dafny","Multi-trace counterexample aggregation boosts Dafny debugging robustness","Dafny fault localization: counterexample structure matters most"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["Counterexample ranking cuts Dafny fault search by two-thirds","Structured counterexample paths beat state snapshots in Dafny","Multi-trace counterexample aggregation boosts Dafny debugging robustness","Dafny fault localization: counterexample structure matters most"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000592,"raw_usage":{"total_tokens":2854,"prompt_tokens":1106,"completion_tokens":1748,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":722,"completion_tokens_details":{"reasoning_tokens":1677}},"tokens_in":722,"tokens_out":1748,"duration_ms":14937,"temperature":1.0,"reasoning_tokens":1677,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-10T04:26:21.480182+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[{"cited_title":"Automated fixing of programs with contracts,","cited_arxiv_id":null,"evidence_quote":"Supplies the AutoFix snapshot methodology that SNAP replicates as the state-based comparison paradigm."},{"cited_title":"Mutdafny: A mutation-based approach to assess dafny specifications,","cited_arxiv_id":null,"evidence_quote":"Contributes the MutDafny mutation operators used to generate the faulty programs that serve as ground truth."}],"review_version":2}