Pith. sign in

REVIEW 4 major objections 6 minor 44 references

Training code models on correct programs and mutants teaches them to insert executable mid-program assertions that catch faults and improve repair.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

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

T0 review · grok-4.5

2026-07-11 20:45 UTC pith:V7ISWL26

load-bearing objection Solid SE methods paper: verification-guided training for executable intermediate assertions, real HumanExec human-bug benchmark, clear gains on checkpoint quality; completeness headline is mutant-proxy heavy and repair transfer is modest. the 4 major comments →

arxiv 2607.04232 v1 pith:V7ISWL26 submitted 2026-07-05 cs.SE cs.CL

Teaching Code LLMs to Reason with Intermediate Formal Specifications

Minh Le-Anh , Cuong Chi Le , Tien N. Nguyen This is my paper
classification cs.SE cs.CL
keywords executable specificationscheckpoint assertionsCodeLLMsspecification generationprogram repairverification-guided trainingHumanExecintermediate formal specifications
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

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

This paper claims that code language models should generate executable checkpoint specifications: Boolean assertions placed at meaningful internal program points that describe expected intermediate states and can be checked on real runs. Prompting alone is not enough; current models often emit assertions that are invalid, trivial, or too weak to reject behavior-changing faults. SpecCoder builds training data from validated reference solutions, filtered one-line mutants, and multi-turn refinement that keeps only assertions which hold on correct executions while rejecting eligible faulty ones. On HumanExec, a benchmark of recent competitive-programming problems with real human buggy submissions, the trained models produce substantially more correct, complete, and valid inline assertions, and those same checks supply evidence that improves program correctness judgments and automated repair. A sympathetic reader cares because intermediate machine-checkable commitments turn vague model reasoning into fine-grained, run-time evidence of where an algorithm first goes wrong.

Core claim

SpecCoder shows that verification-guided fine-tuning—using validated reference programs, behavior-changing mutants that sometimes pass and sometimes fail tests, and an Explore–Submit refinement loop that accepts only assertions meeting high correctness and completeness thresholds—teaches CodeLLMs to generate inline executable checkpoint specifications far stronger than those from prompting the same base models, and that these checkpoints provide usable evidence for correctness checking and program repair on human bugs.

What carries the argument

SpecCoder: a verification-guided training framework that constructs supervision from reference programs, retained non-trivial mutants, and multi-turn specification-refinement traces so accepted assertions hold on correct runs (Corr ≥ α) while rejecting eligible faulty executions that reach the same checkpoint (Comp ≥ β).

Load-bearing premise

The method assumes that filtered one-line mutants which pass at least one test and fail at least one test are a good enough proxy for real human bugs when deciding which intermediate assertions are discriminative.

What would settle it

On a held-out set of human buggy programs, measure whether SpecCoder checkpoints fail on buggy runs at rates far above the base model; if completeness against real human faults stays near the untrained baseline while final-test repair gains disappear, the central claim fails.

Watch this falsifier — get emailed when new claim-graph text bears on it.

If this is right

  • Executable intermediate assertions can replace natural-language state descriptions as the primary automated signal for verification, consistency checking, and repair.
  • A model can instrument a given program so checks fire at the first semantic deviation rather than only when final output is wrong.
  • Correctness checkers and repair agents that consume violated-assertion evidence outperform free-form chain-of-thought or natural-language specification methods under matched budgets.
  • Competitive-programming tasks with real human submissions become a practical testbed for specification quality beyond synthetic mutants.
  • The same training recipe continues to lift both checkpoint quality and downstream repair success as backbone size increases.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The mutant-and-execution filter could be run at inference time as a search over candidate assertions, not only during fine-tuning data construction.
  • Intermediate checkpoints may also help fault localization and stepwise explanation without requiring a full repair loop.
  • If completeness against one-line mutants generalizes poorly to multi-line or design-level bugs, mixing real human-bug traces into training is the natural next experiment.
  • The work points toward a default model output format of code plus machine-checkable intermediate commitments rather than bare code alone.

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

4 major / 6 minor

Summary. The paper proposes SpecCoder, a verification-guided fine-tuning framework that teaches CodeLLMs to insert executable intermediate checkpoint assertions into programs. Training supervision is built from validated reference solutions, one-line behavior-changing mutants, and multi-turn Explore–Submit refinement under execution feedback (correctness Corrij and completeness Compij with thresholds α, β). The authors introduce HumanExec, a Codeforces-based benchmark with reference solutions, test suites, and real human buggy submissions, and evaluate three tasks: checkpoint specification generation, program correctness checking, and program repair. On Qwen2.5-Coder 7B/14B/32B, SpecCoder reports large gains in inline assertion correctness, mutant-based completeness, and validity (Table II), with smaller but positive gains for AssertChecker (Table III) and AssertRepair (Table IV) relative to zero-shot, CoT, HoarePrompt, and SpecRover baselines.

Significance. If the results hold under broader evaluation, the work is a solid contribution to executable intermediate specifications for LLM-based verification. The framing of checkpoints as machine-checkable intermediate evidence, the mutant-guided data pipeline, and HumanExec (real human bugs, problem-level separation from training) are useful for the community. Strengths include execution-based metrics, explicit train/test problem-level separation, evaluation-only mutants for RQ1 completeness, multi-scale Qwen2.5-Coder experiments, and public data/code. The largest reported lifts are in specification quality; downstream checking and repair gains are more modest but directionally consistent with the thesis that executable intermediate evidence helps.

major comments (4)
  1. [Table II, §III.A.3, §V.A] Table II and §V.A.2–3: Completeness (Compij, §III.A.3) is defined and reported exclusively against retained one-line mutants (pass ≥1 and fail ≥1 test; mutated line before checkpoint and co-reachable). HumanExec’s human buggy submissions motivate the benchmark and are used in RQ2/RQ3, but RQ1 completeness is not measured against those real faults. The headline completeness lifts (+358.1% / +287.8% / +159.2%) therefore risk overstating general discriminative power. Please either (i) report completeness / rejection rates of generated checkpoints on HumanExec human bugs (with a clear eligibility rule for multi-line faults), or (ii) substantially temper abstract/intro claims that completeness gains demonstrate intermediate-spec power beyond the mutant proxy.
  2. [Abstract, Table III, Table IV, §V.B–C] Abstract and §I claim that specification gains “further translate” to reliable verification via correctness checking and repair. Tables III–IV show real but modest effects: MCC gains of roughly +0.07–0.10 over Vanilla, and Pass@1 gains of about +0.004–0.051, with AssertRepair not uniformly dominating SpecRover/HoarePrompt on all metrics (e.g., 7B APR, 32B Pass@3). The causal link from higher Compij to better human-bug diagnosis is asserted more strongly than the effect sizes support. Please quantify how often violated checkpoints localize the human bug, or present ablations that isolate executable-assertion evidence from other prompt content.
  3. [§III.A.2–3, Algorithm 1] §III.A.2–3 and Algorithm 1: Training and evaluation completeness both rely on the same operational mutant filter (one-line edits, ≥1 pass and ≥1 fail, eligibility by line order and co-reachability). This is a coherent proxy, but it is also the paper’s weakest load-bearing assumption for “discriminative intermediate specifications.” Without evidence that mutant-selected checkpoints reject multi-line / design-level human faults at similar rates, the completeness story remains partly in-distribution. A short human-bug rejection study or failure analysis would make the central claim much more robust.
  4. [§V.2, Tables II–IV] §V.2 and Tables II–IV: All main results use only the Qwen2.5-Coder family. The framework is presented as general for CodeLLMs, but architecture/family dependence is untested. At least one additional backbone (or a clear limitation statement with reduced claims) is needed for the generality implied by the title and abstract.
minor comments (6)
  1. [§III.A.3] §III.A.3: Default thresholds α=1.0 and β=0.9, max turns K, and the >30-test filter are free parameters. A brief sensitivity analysis (or appendix) would strengthen confidence that results are not brittle to these choices.
  2. [Fig. 5] Fig. 5 / qualitative example is helpful, but the figure text is dense and hard to parse in the manuscript layout; consider a cleaner side-by-side with fewer comments and highlighted assertion lines.
  3. [Table I, Table II] Table I vs Table II: Table I appears to reuse HumanExec-style metrics for base models “before fine-tuning”; clarify whether Table I is exactly the zero-shot HumanEval/HumanExec baseline later expanded in Table II, to avoid double-counting confusion.
  4. [§IV] §IV: HumanExec statistics (150 tasks, difficulty 800–2500, mutant counts) are useful; please also state train/test split sizes for the LeetCode-style training corpus and whether any Codeforces problems overlap with common pretraining sources (even if only as a limitation).
  5. [Throughout] Notation: SpecCoder is inconsistently spaced/capitalized (SPECCODER / SpecCoder / SPECCODERselects). Normalize throughout.
  6. [§VI] Related work is generally appropriate; a short explicit comparison to classical dynamic invariant tools (e.g., Daikon-style) on the same checkpoint task would help readers place the contribution.

Circularity Check

0 steps flagged

No circular derivation: SpecCoder optimizes and evaluates held-out execution metrics; completeness is an operational mutant proxy, not a fitted quantity renamed as prediction.

full rationale

This is an empirical SE/ML paper, not a first-principles derivation. Training accepts assertions only when they hold on validated reference executions (Corr_ij ≥ α) and reject retained one-line mutants (Comp_ij ≥ β), then converts accepted annotated programs into SFT targets. Evaluation is on HumanExec, built from recent Codeforces problems kept separate from the LeetCode-style training corpus, with problem-level splits before mutant generation. RQ1 completeness uses evaluation-only mutants generated after the split and never used in training; correctness and validity are independent execution checks. Downstream RQ2/RQ3 use real human buggy submissions, not the training mutants. SpecMind is cited only as methodological inspiration for multi-turn refinement, not as a uniqueness theorem that forces the result. There is no self-definitional equation, no parameter fitted on a subset and re-reported as a prediction, and no load-bearing self-citation chain. Measuring large completeness lifts on a mutant-rejection metric that matches the training filter is expected optimization success under held-out generalization, not circularity by construction. The paper itself states completeness is operational against available faulty executions rather than logical completeness over all bugs. Score 0.

Axiom & Free-Parameter Ledger

4 free parameters · 4 axioms · 3 invented entities

This is an empirical SE/ML methods paper. The central claim rests on execution-based acceptance of teacher-generated assertions, hand-chosen quality thresholds, and the assumption that one-line non-trivial mutants plus available test suites adequately supervise and score intermediate specifications. No physical constants or deep mathematical postulates; the free parameters are design thresholds and filtering rules.

free parameters (4)
  • correctness threshold α
    Default α=1.0 required for every assertion on reference executions before accepting a trajectory as training data (§III.A.3).
  • completeness threshold β
    Default β=0.9 required for assertions with evaluable mutant sets; hand-chosen acceptance gate for supervision quality.
  • maximum refinement turns K
    Caps multi-turn Explore–Submit; unsuccessful trajectories are discarded if thresholds are unmet.
  • minimum test-suite size filter (>30 tests)
    Problem selection rule that determines which reference programs enter data construction (§III.A.1).
axioms (4)
  • domain assumption A non-trivial mutant that passes at least one test and fails at least one test provides useful intermediate fault signal rather than equivalence or total breakage.
    Used to retain Mi in §III.A.2; completeness and training negatives depend on this filter.
  • domain assumption Eligible mutants for a checkpoint are only those whose changed line occurs before the checkpoint and can co-reach it.
    Defines Comp_ij in §III.A.3; without this, completeness scores would be ill-posed.
  • domain assumption Passing the available test suite is sufficient to treat a submission as a trusted reference implementation for correct intermediate states.
    Reference validation step in §III.A.1; all correctness labels for assertions rest on this.
  • ad hoc to paper Teacher multi-turn refinement under execution feedback yields supervision targets worth imitating by the student.
    Core of SpecCoder data construction; student never sees exploration traces, only accepted annotated programs.
invented entities (3)
  • SpecCoder training framework independent evidence
    purpose: Package mutant-guided multi-turn refinement into SFT for checkpoint-annotated code generation and annotation.
    Primary method contribution; independent evidence is the empirical HumanExec evaluation, not external theory.
  • HumanExec benchmark independent evidence
    purpose: Provide Codeforces-based tasks with human buggy submissions for specification generation, correctness checking, and repair.
    New evaluation resource claimed separate from LeetCode-style training data; usefulness is demonstrated only within this paper’s experiments.
  • Executable checkpoint specification task framing no independent evidence
    purpose: Treat intermediate assert insertion as the primary specification target rather than whole-program pre/postconditions or natural-language states.
    Conceptual framing that organizes the method and metrics; related ideas exist, but this packaging is paper-specific.

pith-pipeline@v1.1.0-grok45 · 24274 in / 3151 out tokens · 46819 ms · 2026-07-11T20:45:41.580888+00:00 · methodology

0 comments
read the original abstract

Unlike natural-language specifications, executable formal specifications provide machine-checkable constraints for verifying, debugging, and repairing code. However, writing such specifications is labor-intensive, and existing LLM-based methods mainly infer whole-program pre/postconditions, missing the intermediate semantic commitments that programmers rely on when reasoning about an algorithm. Our study further shows that prompting current CodeLLMs often produces executable assertions that are syntactically invalid, trivial, or too weak to reject behavior-changing faults. In this paper, we study executable checkpoint specification generation, where assertions are inserted at meaningful internal program points to describe expected intermediate states. We introduce SpecCoder, a verification-guided CodeLLM training framework that learns from validated reference programs, behavior-changing mutants, and multi-turn specification-refinement traces. SpecCoder selects specifications that hold on correct executions while rejecting faulty executions, turning specifications from passive annotations into executable evidence. To evaluate this setting, we introduce HumanExec, a benchmark built from recent Codeforces competitive programming problems with test suites, reference solutions, and human buggy submissions, supporting three tasks: specification generation, program correctness checking, and program repair. Experiments on HumanExec show that SpecCoder substantially improves checkpoint-specification quality over base CodeLLMs. Across Qwen2.5-Coder models, SpecCoder improves inline-specification correctness by up to 55.8%, completeness by up to 358.1%, and executable assertion validity by up to 26.6%. These gains further translate to downstream correctness reasoning and repair, showing that executable checkpoints provide fine-grained evidence for reliable verification.

Figures

Figures reproduced from arXiv: 2607.04232 by Cuong Chi Le, Minh Le-Anh, Tien N. Nguyen.

Figure 1
Figure 1. Figure 1: Natural-language versus Executable Checkpoint Specification [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Pipeline for mutant-guided checkpoint specification data construction. [PITH_FULL_IMAGE:figures/full_fig_p004_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Quality of generated checkpoint assertions. [PITH_FULL_IMAGE:figures/full_fig_p007_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: ECDF of per-assertion perplexity on held-out inline checkpoint [PITH_FULL_IMAGE:figures/full_fig_p008_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Qualitative comparison of specification generation [PITH_FULL_IMAGE:figures/full_fig_p009_5.png] view at source ↗

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

44 extracted references · 4 canonical work pages

  1. [1]

    Leveraging existing instrumentation to automatically infer invariant-constrained models,

    I. Beschastnikh, Y . Brun, S. Schneider, M. Sloan, and M. D. Ernst, “Leveraging existing instrumentation to automatically infer invariant-constrained models,” inProceedings of the 19th Symposium on Foundations of Software Engineering, ser. ESEC/FSE ’11. ACM, 2011, pp. 267–277. [Online]. Available: http://doi.acm.org/10.1145/2025113.2025151

    doi:10.1145/2025113.2025151 2011

  2. [2]

    Dynamically discovering likely program invariants to support program evolution,

    M. D. Ernst, J. Cockrell, W. G. Griswold, and D. Notkin, “Dynamically discovering likely program invariants to support program evolution,” inProceedings of the 21st International Conference on Software Engineering, ser. ICSE’99. ACM, 1999, pp. 213–224. [Online]. Available: http://doi.acm.org/10.1145/302405.302467

    doi:10.1145/302405.302467 1999

  3. [3]

    Can large language models transform natural language intent into formal method postconditions?

    M. Endres, S. Fakhoury, S. Chakraborty, and S. K. Lahiri, “Can large language models transform natural language intent into formal method postconditions?”Proc. ACM Softw. Eng., vol. 1, no. FSE, Jul. 2024. [Online]. Available: https://doi.org/10.1145/3660791

    doi:10.1145/3660791 2024

  4. [4]

    SpecMind: Cognitively inspired, interactive multi-turn framework for postcondition inference,

    C. C. Le, M. V . Pham, T. D. Vu, V . D. Cuong, P. N. Huy, P. N. Hoang, and T. N. Nguyen, “SpecMind: Cognitively inspired, interactive multi-turn framework for postcondition inference,” inProceedings of the 64th Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), M. Liakata, V . P. Moreira, J. Zhang, and D. Jurgens, Eds...

    2026

  5. [5]

    Hoareprompt: Structural reasoning about program correctness in natural language,

    D. S. Bouras, Y . Dai, T. Wang, Y . Xiong, and S. Mechtaev, “Hoareprompt: Structural reasoning about program correctness in natural language,” 2025. [Online]. Available: https://arxiv.org/abs/2503.19599

    Pith/arXiv arXiv 2025

  6. [6]

    Specrover: Code intent extraction via llms,

    H. Ruan, Y . Zhang, and A. Roychoudhury, “Specrover: Code intent extraction via llms,” inProceedings of the IEEE/ACM 47th International Conference on Software Engineering, ser. ICSE ’25. IEEE Press, 2025, p. 963–974. [Online]. Available: https://doi.org/10.1109/ICSE55347.2025.00080

    doi:10.1109/icse55347.2025.00080 2025

  7. [7]

    Mining specifications,

    G. Ammons, R. Bod ´ık, and J. R. Larus, “Mining specifications,” inProceedings of the 29th ACM SIGPLAN SIGACT Symposium on Principles of Programming Languages, ser. POPL ’02. ACM, 2002, pp. 4–16. [Online]. Available: http://doi.acm.org/10.1145/503272.503275

    doi:10.1145/503272.503275 2002

  8. [8]

    Static specification mining using automata-based abstractions,

    S. Shoham, E. Yahav, S. Fink, and M. Pistoia, “Static specification mining using automata-based abstractions,” inProceedings of the 2007 International Symposium on Software Testing and Analysis, ser. ISSTA ’07. New York, NY , USA: Association for Computing Machinery, 2007, p. 174–184. [Online]. Available: https://doi.org/10.1145/1273463.1273487

    work page doi:10.1145/1273463.1273487 2007

  9. [9]

    Bugs as deviant behavior: A general approach to inferring errors in systems code,

    D. Engler, D. Y . Chen, S. Hallem, A. Chou, and B. Chelf, “Bugs as deviant behavior: A general approach to inferring errors in systems code,” inProceedings of the Eighteenth ACM Symposium on Operating Systems Principles, ser. SOSP’01. ACM, 2001, pp. 57–72. [Online]. Available: http://doi.acm.org/10.1145/502034.502041

    doi:10.1145/502034.502041 2001

  10. [10]

    From uncertainty to belief: inferring the specification within,

    T. Kremenek, P. Twohey, G. Back, A. Ng, and D. Engler, “From uncertainty to belief: inferring the specification within,” inProceedings of the 7th Symposium on Operating Systems Design and Implementation, ser. OSDI ’06. USA: USENIX Association, 2006, p. 161–176

    2006

  11. [11]

    Static specification inference using predicate mining,

    M. K. Ramanathan, A. Grama, and S. Jagannathan, “Static specification inference using predicate mining,” inProceedings of the 2007 ACM SIGPLAN Conference on Programming Language Design and Implementation, ser. PLDI ’07. ACM, 2007, pp. 123–134. [Online]. Available: http://doi.acm.org/10.1145/1250734.1250749

    doi:10.1145/1250734.1250749 2007

  12. [12]

    Inferring better contracts,

    Y . Wei, C. A. Furia, N. Kazmin, and B. Meyer, “Inferring better contracts,” inProceedings of the 33rd International Conference on Software Engineering, ser. ICSE ’11. ACM, 2011, pp. 191–200. [Online]. Available: http://doi.acm.org/10.1145/1985793.1985820

    work page doi:10.1145/1985793.1985820 2011

  13. [13]

    An abstract interpretation framework for refactoring with application to extract methods with contracts,

    P. M. Cousot, R. Cousot, F. Logozzo, and M. Barnett, “An abstract interpretation framework for refactoring with application to extract methods with contracts,” inProceedings of the ACM International Conference on Object Oriented Programming Systems Languages and Applications, ser. OOPSLA ’12. New York, NY , USA: Association for Computing Machinery, 2012, ...

    doi:10.1145/2384616.2384633 2012

  14. [14]

    Inferring method specifications from natural language api descriptions,

    R. Pandita, X. Xiao, H. Zhong, T. Xie, S. Oney, and A. Paradkar, “Inferring method specifications from natural language api descriptions,” inProceedings of the 34th International Conference on Software Engi- neering, ser. ICSE ’12. IEEE Press, 2012, p. 815–825

    2012

  15. [15]

    /*icomment: bugs or bad comments?*/,

    L. Tan, D. Yuan, G. Krishna, and Y . Zhou, “/*icomment: bugs or bad comments?*/,” inProceedings of Twenty-First ACM SIGOPS Symposium on Operating Systems Principles, ser. SOSP ’07. New York, NY , USA: Association for Computing Machinery, 2007, p. 145–158. [Online]. Available: https://doi.org/10.1145/1294261.1294276

    doi:10.1145/1294261.1294276 2007

  16. [16]

    acomment: mining annotations from comments and code to detect interrupt related concurrency bugs,

    L. Tan, Y . Zhou, and Y . Padioleau, “acomment: mining annotations from comments and code to detect interrupt related concurrency bugs,” inProceedings of the 33rd International Conference on Software Engineering, ser. ICSE ’11. New York, NY , USA: Association for Computing Machinery, 2011, p. 11–20. [Online]. Available: https://doi.org/10.1145/1985793.1985796

    doi:10.1145/1985793.1985796 2011

  17. [17]

    @tcomment: Testing javadoc comments to detect comment-code inconsistencies,

    S. H. Tan, D. Marinov, L. Tan, and G. T. Leavens, “@tcomment: Testing javadoc comments to detect comment-code inconsistencies,” inProceedings of the 2012 IEEE Fifth International Conference on Software Testing, Verification and Validation, ser. ICST ’12. USA: IEEE Computer Society, 2012, p. 260–269. [Online]. Available: https://doi.org/10.1109/ICST.2012.106

    doi:10.1109/icst.2012.106 2012

  18. [18]

    Translating code comments to procedure specifications,

    A. Blasi, A. Goffi, K. Kuznetsov, A. Gorla, M. D. Ernst, M. Pezz `e, and S. D. Castellanos, “Translating code comments to procedure specifications,” inProceedings of the 27th ACM SIGSOFT International Symposium on Software Testing and Analysis, ser. ISSTA 2018. New York, NY , USA: Association for Computing Machinery, 2018, p. 242–253. [Online]. Available:...

    doi:10.1145/3213846.3213872 2018

  19. [19]

    Inferring resource specifications from natural language api documentation,

    H. Zhong, L. Zhang, T. Xie, and H. Mei, “Inferring resource specifications from natural language api documentation,” inProceedings of the 24th IEEE/ACM International Conference on Automated Software Engineering, ser. ASE ’09. USA: IEEE Computer Society, 2009, p. 307–318. [Online]. Available: https://doi.org/10.1109/ASE.2009.94

    doi:10.1109/ase.2009.94 2009

  20. [20]

    Analyzing apis documentation and code to detect directive defects,

    Y . Zhou, R. Gu, T. Chen, Z. Huang, S. Panichella, and H. Gall, “Analyzing apis documentation and code to detect directive defects,” in2017 IEEE/ACM 39th International Conference on Software Engi- neering (ICSE), 2017, pp. 27–37

    2017

  21. [21]

    Pr-miner: Automatically extracting implicit programming rules and detecting violations in large software code,

    Z. Li and Y . Zhou, “Pr-miner: Automatically extracting implicit programming rules and detecting violations in large software code,” inProceedings of the 13th Symposium on Foundations of Software Engineering, ser. ESEC/FSE-13. ACM, 2005, pp. 306–315. [Online]. Available: http://doi.acm.org/10.1145/1081706.1081755

    doi:10.1145/1081706.1081755 2005

  22. [22]

    Dynamine: finding common error patterns by mining software revision histories,

    B. Livshits and T. Zimmermann, “Dynamine: finding common error patterns by mining software revision histories,” inProceedings of the 10th European Software Engineering Conference Held Jointly with 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering, ser. ESEC/FSE-13. New York, NY , USA: Association for Computing Machinery, 2005...

    doi:10.1145/1081706.1081754 2005

  23. [23]

    Mapo: Mining and recommending api usage patterns,

    H. Zhong, T. Xie, L. Zhang, J. Pei, and H. Mei, “Mapo: Mining and recommending api usage patterns,” inProceedings of the 23rd Euro- pean Conference on ECOOP 2009 — Object-Oriented Programming. Springer-Verlag, 2009, pp. 318–343

    2009

  24. [24]

    Detecting object usage anomalies,

    A. Wasylkowski, A. Zeller, and C. Lindig, “Detecting object usage anomalies,” inProceedings of the Symposium on Foundations of Software Engineering, ser. ESEC-FSE ’07. ACM, 2007, pp. 35–44. [Online]. Available: http://doi.acm.org/10.1145/1287624.1287632

    doi:10.1145/1287624.1287632 2007

  25. [25]

    Automatic mining of source code repositories to improve bug finding techniques,

    C. C. Williams and J. K. Hollingsworth, “Automatic mining of source code repositories to improve bug finding techniques,”IEEE Trans. Softw. Eng., vol. 31, no. 6, pp. 466–480, 2005

    2005

  26. [26]

    Alattin: Mining alternative patterns for detecting neglected conditions,

    S. Thummalapenta and T. Xie, “Alattin: Mining alternative patterns for detecting neglected conditions,” inProceedings of the 2009 IEEE/ACM International Conference on Automated Software Engineering, ser. ASE ’09. IEEE Computer Society, 2009, pp. 283–294. [Online]. Available: http://dx.doi.org/10.1109/ASE.2009.72

    doi:10.1109/ase.2009.72 2009

  27. [27]

    Graph-based mining of multiple object usage patterns,

    T. T. Nguyen, H. A. Nguyen, N. H. Pham, J. M. Al-Kofahi, and T. N. Nguyen, “Graph-based mining of multiple object usage patterns,” in Proceedings of the Symposium on Foundations of Software Engineering, ser. ESEC/FSE ’09. ACM, 2009, pp. 383–392. [Online]. Available: http://doi.acm.org/10.1145/1595696.1595767

    doi:10.1145/1595696.1595767 2009

  28. [28]

    Automatic generation of object usage specifications from large method traces,

    M. Pradel and T. R. Gross, “Automatic generation of object usage specifications from large method traces,” inProceedings of the 2009 IEEE/ACM International Conference on Automated Software Engineering, ser. ASE ’09. IEEE Computer Society, 2009, pp. 371–382. [Online]. Available: http://dx.doi.org/10.1109/ASE.2009.60

    work page doi:10.1109/ase.2009.60 2009

  29. [29]

    Mining temporal specifications from object usage,

    A. Wasylkowski and A. Zeller, “Mining temporal specifications from object usage,” inProceedings of the 2009 IEEE/ACM International Conference on Automated Software Engineering, ser. ASE ’09. IEEE Computer Society, 2009, pp. 295–306. [Online]. Available: http://dx.doi.org/10.1109/ASE.2009.30

    work page doi:10.1109/ase.2009.30 2009

  30. [30]

    Toga: a neural method for test oracle generation,

    E. Dinella, G. Ryan, T. Mytkowicz, and S. K. Lahiri, “Toga: a neural method for test oracle generation,” inProceedings of the 44th International Conference on Software Engineering, ser. ICSE ’22. New York, NY , USA: Association for Computing Machinery, 2022, p. 2130–2141. [Online]. Available: https://doi.org/10.1145/3510003.3510141

    doi:10.1145/3510003.3510141 2022

  31. [31]

    Using transfer learning for code- related tasks,

    A. Mastropaolo, N. Cooper, D. N. Palacio, S. Scalabrino, D. Poshy- vanyk, R. Oliveto, and G. Bavota, “Using transfer learning for code- related tasks,”IEEE Transactions on Software Engineering, vol. 49, no. 4, pp. 1580–1598, 2023

    2023

  32. [32]

    Generating accurate assert statements for unit test cases using pretrained transformers,

    M. Tufano, D. Drain, A. Svyatkovskiy, and N. Sundaresan, “Generating accurate assert statements for unit test cases using pretrained transformers,” inProceedings of the 3rd ACM/IEEE International Conference on Automation of Software Test, ser. AST ’22. New York, NY , USA: Association for Computing Machinery, 2022, p. 54–64. [Online]. Available: https://do...

    doi:10.1145/3524481.3527220 2022

  33. [33]

    Interactive code generation via test-driven user-intent formalization,

    S. K. Lahiri, S. Fakhoury, A. Naik, G. Sakkas, S. Chakraborty, M. Musuvathi, P. Choudhury, C. von Veh, J. P. Inala, C. Wang, and J. Gao, “Interactive code generation via test-driven user-intent formalization,” 2023. [Online]. Available: https://arxiv.org/abs/2208.05950

    Pith/arXiv arXiv 2023

  34. [34]

    Unit test case generation with transformers and focal context,

    M. Tufano, D. Drain, A. Svyatkovskiy, S. K. Deng, and N. Sundaresan, “Unit test case generation with transformers and focal context,” 2021. [Online]. Available: https://arxiv.org/abs/2009.05617

    Pith/arXiv arXiv 2021

  35. [35]

    Codamosa: Escaping coverage plateaus in test generation with pre-trained large language models,

    C. Lemieux, J. P. Inala, S. K. Lahiri, and S. Sen, “Codamosa: Escaping coverage plateaus in test generation with pre-trained large language models,” inProceedings of the 45th International Conference on Software Engineering, ser. ICSE ’23. IEEE Press, 2023, p. 919–931. [Online]. Available: https://doi.org/10.1109/ICSE48619.2023.00085

    doi:10.1109/icse48619.2023.00085 2023

  36. [36]

    Coverup: Effective high coverage test generation for python,

    J. Altmayer Pizzorno and E. D. Berger, “Coverup: Effective high coverage test generation for python,”Proc. ACM Softw. Eng., vol. 2, no. FSE, Jun. 2025. [Online]. Available: https://doi.org/10.1145/3729398

    doi:10.1145/3729398 2025

  37. [37]

    Evospex: An evolutionary algorithm for learning postconditions,

    F. Molina, P. Ponzio, N. Aguirre, and M. Frias, “Evospex: An evolutionary algorithm for learning postconditions,” inProceedings of the 43rd International Conference on Software Engineering, ser. ICSE ’21. IEEE Press, 2021, p. 1223–1235. [Online]. Available: https://doi.org/10.1109/ICSE43902.2021.00112

    doi:10.1109/icse43902.2021.00112 2021

  38. [38]

    Can large language models write good property-based tests?

    V . Vikram, C. Lemieux, J. Sunshine, and R. Padhye, “Can large language models write good property-based tests?” 2024. [Online]. Available: https://arxiv.org/abs/2307.04346

    Pith/arXiv arXiv 2024

  39. [39]

    Toward trustworthy neural program synthesis,

    W.-D. Li, D. Y . Key, and K. Ellis, “Toward trustworthy neural program synthesis,” inICLR 2025 Third Workshop on Deep Learning for Code, 2025. [Online]. Available: https://openreview.net/forum?id=zC4Wjyu2Wu

    2025

  40. [40]

    Learning invariants using decision trees and implication counterexamples,

    P. Garg, D. Neider, P. Madhusudan, and D. Roth, “Learning invariants using decision trees and implication counterexamples,” inProceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, ser. POPL ’16. New York, NY , USA: Association for Computing Machinery, 2016, p. 499–512. [Online]. Available: https://doi.org/10.1...

    doi:10.1145/2837614.2837664 2016

  41. [41]

    Guiding program synthesis by learning to generate examples,

    L. Laich, P. Bielik, and M. Vechev, “Guiding program synthesis by learning to generate examples,” inInternational Conference on Learning Representations, 2020. [Online]. Available: https://openreview.net/forum?id=BJl07ySKvS

    2020

  42. [42]

    Learning nonlinear loop invariants with gated continuous logic networks,

    J. Yao, G. Ryan, J. Wong, S. Jana, and R. Gu, “Learning nonlinear loop invariants with gated continuous logic networks,” inProceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation, ser. PLDI 2020. New York, NY , USA: Association for Computing Machinery, 2020, p. 106–120. [Online]. Available: https://doi.org/10.1145/...

    doi:10.1145/3385412.3385986 2020

  43. [43]

    Can large language models reason about program invariants?

    K. Pei, D. Bieber, K. Shi, C. Sutton, and P. Yin, “Can large language models reason about program invariants?” inProceedings of the 40th International Conference on Machine Learning, ser. Proceedings of Machine Learning Research, A. Krause, E. Brunskill, K. Cho, B. Engelhardt, S. Sabato, and J. Scarlett, Eds., vol. 202. PMLR, 23–29 Jul 2023, pp. 27 496–27...

    2023

  44. [44]

    Available: https://speccoder.site

    [Online]. Available: https://speccoder.site