Do AI models help produce verified bug fixes?

Alessandro Schena; Bertrand Meyer; Ilgiz Mustafin; Li Huang; Marco Piccioni; Reto Weber

REVIEW 3 major objections 6 minor 36 references

Do AI models help produce verified bug fixes?

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

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

Pith's one-line read A controlled 25-person experiment found that giving programmers access to GPT-4o mini did not improve their verified bug fixes: the no-LLM group performed better or as well on most measures.

desk verdict A proof-validated debugging study with a genuinely useful qualitative taxonomy, but the headline 'no benefit from LLM' is underpowered by a small, unbalanced sample. read the letter →

arxiv 2507.15822 v2 pith:GCTORMDD submitted 2025-07-21 cs.SE cs.AI

Li Huang , Ilgiz Mustafin , Marco Piccioni , Alessandro Schena , Reto Weber , Bertrand Meyer This is my paper

classification cs.SEcs.AI

keywords AutomaticProgramRepairLLM-assisteddebuggingformalverificationGPT-4ominiGoal-Question-MetrichallucinationloopprogrammerinteractionpatternsEiffelcontracts

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

This paper asks whether programmers who can consult a large language model actually produce better bug fixes when correctness is judged by a formal program prover instead of by tests. The experiment assigned 25 volunteers to either an LLM-assisted group (with GPT-4o mini) or a no-LLM control group and gave both the same nine buggy Eiffel programs, with every proposed fix checked by the AutoProof verifier. The central claim is that, on most measures, LLM access did not help: programmers without the LLM solved more tasks correctly and fewer incorrectly, while LLM users often fell into 'hallucination loops' in which confident wrong suggestions consumed time. The paper's value for a general reader is that it replaces anecdote with a setting where 'correct fix' is an objective, proof-backed outcome, and it maps the interaction patterns that separate helpful from harmful AI use.

What carries the argument

The load-bearing object is the AutoProof program verifier, backed by Boogie and the Z3 SMT solver, which checks an Eiffel program annotated with contracts (preconditions, postconditions, class invariants) and returns a proof or a counterexample; this makes 'verified fix' a binary, objective outcome rather than a judgment based on test cases. The study's methodological machinery is the Goal-Question-Metric decomposition of the two research questions into six queries and a set of numeric metrics, fixed before the experiment to avoid post-hoc hypotheses. The observation machinery is full-session screen recording of each participant, from which the authors derived seven categories of prompts and six programmer 'personalities' (independent, prejudiced, searcher, copy-paster, follower, collaborator, with quitter as a terminal state). These patterns carry the qualitative conclusions about which uses of LLMs help and which harm.

What would settle it

The central claim would be refuted by a replication with a larger, experience-balanced sample, say 100 participants per arm, in which the LLM-assisted group solves significantly more tasks correctly, in less time, and with fewer incorrect submissions than the no-LLM control; the current sample is too small to rule that outcome out.

Watch

Extended reading notes

Core claim

The paper's central claim, stated as its main lesson, is that 'whatever their merits for debugging, LLMs (at least to judge by GPT-4o mini's performance) are not a silver bullet'; programmers not using the LLM performed better or as well on most counts. This conclusion comes from a randomized comparison in which the no-LLM group solved more tasks correctly and fewer incorrectly, while LLM-assisted participants spent substantial time in hallucination loops, and copy-pasting an LLM-generated fix was part of the final accepted solution exactly once. The claim carries two qualifications: complete novices could benefit from the LLM for identifying and correcting simple bugs, and programmers already expert in the language could sometimes use it to zoom in faster on a solution. The paper also asserts that a 'collaborator' pattern of interaction, in which the programmer feeds both code and verifier output to the LLM, asks for a diff, and reviews the suggestion, was the most effective observed strategy.

Load-bearing premise

The load-bearing premise is that randomly assigning only 25 volunteers produced comparable groups, even though experience was not balanced and all four no-shows came from the LLM-assisted group; if the groups differed in skill or motivation, the LLM group's disadvantages would not be caused by LLM use.

Editorial extensions

If this is right

Because fix validity is decided by a prover, this setup removes the overfitting risk that plagues test-based APR evaluation and can serve as a reusable methodology for future LLM debugging studies.
For the average participant in this sample, LLM access did not increase the number of correctly solved tasks and was associated with more incorrect submissions.
LLM help appears concentrated at the two extremes of expertise: complete novices fixing simple bugs, and language experts who can quickly filter good from bad suggestions.
Hallucination loops are a measurable cost: they consume time on hard tasks, and copy-pasted LLM code was part of the final accepted fix only once across all sessions.
The collaborator pattern, which sends code plus verifier output, asks for a diff, and reviews before submitting, had the highest observed success rate and is the basis of the paper's recommended strategy.

Reading between the lines

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

A natural engineering extension would be an IDE plugin that automatically bundles the verifier's counterexample with the code, asks the LLM for a minimal diff, and marks which suggested lines actually verify.
The results imply an inverted-U pattern: LLM help assists novices on trivial bugs, adds little for average programmers, and mainly saves time for experts; stratifying tasks by difficulty in a larger sample could test this directly.
Since only GPT-4o mini was used, the conclusion is model-specific; repeating the protocol with stronger or reasoning-focused models would show whether the negative result is a property of LLM assistance in general or of this model.
The observed noise in LLM answers suggests a concrete, testable improvement target: forcing the model to rank its own suggestions by confidence could attack both the neutrality flaw and the hallucination loop.

Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

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

Desk Editor's Note

read the letter

Here's my take on arXiv:2507.15822. The paper does something genuinely new: it runs a randomized human debugging study where every proposed fix is checked by a formal prover (AutoProof), not just tests. That alone separates it from the Copilot and chatbot user studies. The GQM framework was fixed in advance, the full-session recordings let the authors build a taxonomy of seven interaction patterns (collaborator, copy-paster, etc.), and the qualitative observations like the 'hallucination loop' are vivid and plausible. I give real credit for the transparency: Section 7 explicitly says the numbers do not justify statistical analysis, and Section 8.1 concedes the first chart is too coarse-grained for a conclusion.

The soft spots are exactly where the stress-test note points. The central comparison—10 AI participants vs 15 non-AI—is unbalanced because all four no-shows landed in the AI group, and the paper never reports the per-group experience questionnaires. With that sample, random assignment cannot guarantee comparable groups, so the observed non-AI advantage might be an experience effect, not an LLM effect. The authors themselves hedge in the body, but then Section 10.1 states that 'programmers not using the LLM perform better or as well on most counts.' That conclusion is not supported by the data as presented. The later experience splits are based on even smaller subgroups. Also the 'validated advice' in 9.3 is induced from the same sessions used to evaluate it, so 'validated' overstates the evidence, and the qualitative pattern labels were single-coded. These are real but not fatal for an exploratory study.

Who gets value from this? People studying LLM-based debugging and APR who need a proof-of-concept for proof-validated human studies, and anyone interested in interaction patterns. The methodology is reusable. I'd like to see the authors either collect more participants or explicitly reframe the headline as an exploratory negative result. As is, it deserves a serious referee: the method is novel, the observations are useful, and the flaws are mostly acknowledged. I would not want the paper to be desk-rejected; I'd send it to review with a request for a softer conclusion and more careful group-comparison reporting.

Referee Report

3 major / 6 minor

Summary. The paper reports a randomized experiment with 25 volunteer programmers debugging nine buggy Eiffel programs in a formal-verification environment (AutoProof); one group (n=10 after attrition) had access to GPT-4o mini via duck.ai, while the other (n=15) did not. Using a GQM framework defined in advance, the authors compare number of solved tasks, time, incorrect submissions, and experience-based splits, and supplement the quantitative measures with video-based qualitative analysis that yields prompt categories, usage patterns ("personalities"), antipatterns such as "hallucination loops," and practical advice. The central conclusion is that LLMs are not a silver bullet for verified bug fixes: programmers without LLM access perform better or as well on most counts, except for novices and Eiffel experts, and effective use requires a collaborative, critical process.

Significance. The paper's strengths include a novel use of formal verification to adjudicate fix correctness, a pre-specified GQM query/metric structure, full-session screen recordings that enable rich behavioral observation, and honest disclosure of limitations plus public supplementary materials. If the central comparative claim were statistically supported, it would be an important counterexample to optimistic claims about LLM-based program repair. As it stands, the descriptive results and qualitative taxonomies are valuable exploratory contributions, but the main "whether" conclusion currently exceeds what the data and the paper's own stated analysis can support.

major comments (3)

[§10.1, §7, §8.1] The conclusion in §10.1 that "programmers not using the LLM perform better or as well on most counts" is presented as a clear lesson, but it is not backed by inferential statistics: §7 explicitly states that the paper "refrains from any detailed statistical analysis (which the numbers do not justify)," and §8.1 cautions that the QW-1 result is "too coarse-grained to allow such a conclusion." With only 10 AI-group and 15 non-AI-group participants, the observed differences in solved tasks, time, and incorrect submissions could arise from sampling noise; the paper should either add appropriate statistical tests (e.g., permutation tests with effect sizes and confidence intervals) or explicitly reframe this conclusion as a tentative, exploratory finding.
[§6, §8.1 (QW-5, QW-6)] The group comparison is compromised by unverified comparability: all four no-shows came from the AI group, leaving 10 versus 15 participants after random assignment, and the paper does not report the per-group distribution of the questionnaire's experience and activity measures. Since LLM access is the only systematic difference between groups, any pre-existing imbalance (e.g., in Eiffel or static-verification experience, or motivation) could explain the observed disadvantage of the AI group. The experience-based splits in QW-5 and QW-6 rely on even smaller subgroups and inherit this problem. The paper should report per-group questionnaire summaries, discuss the attrition pattern, and temper the central claim accordingly.
[§9.1, §9.2, §9.3] The qualitative categories (antipatterns, personalities, and prompt categories) are derived from video observation, but no inter-rater reliability or coding procedure is reported; without this, the claim of "validated advice" in §10.2 is not supported. The authors should either report a reliability assessment (e.g., a second coder on a subset with agreement statistics) or remove/weaken the term "validated" and describe the categories as exploratory.

minor comments (6)

[§6] "By a stroke of back luck" should read "bad luck."
[§3, QH-6 footnote] "consideraton" is a typo for "consideration."
[§8.1, QW-4] The metrics MW-4.a/b are defined in §3 as "incorrect features," but the observations and chart report "incorrect tasks"; the terminology should be aligned.
[References [10] and [11]] Both list "Doe, J." with the same title but different URLs; these look like placeholder citations and should be resolved before publication.
[§9.1] "copyppaste" is a typo; "copy-paste" is intended.
[§8 figures] The figures in Section 8 lack captions and axis labels in the provided text; adding them would improve readability.

Circularity Check

1 steps flagged · score 1.0 of 10

No equation-level circularity; only a mild in-sample aspect in the qualitative advice, which does not affect the main group comparison.

other [Sections 9.2-9.3; Abstract's 'validated advice' claim]
"Collaborators had the highest observed success rate ( ˜91%) ... From the present work also emerges a proposed best overall strategy, based on the collaborator personality pattern."

The collaborator pattern is identified from the recorded sessions, its success rate is measured on the same sessions, and the recommended 'best overall strategy' is then defined as that pattern. The abstract calls the resulting advice 'validated', but no held-out or independent confirmation is offered; the advice is an in-sample summary of the data rather than a prediction tested on new evidence. This is a mild, qualitative self-referentiality, not a fitted-parameter or equation-level reduction, and it does not underpin the LLM/no-LLM task-outcome comparison, which rests on externally defined correctness of fixes.

full rationale

The paper's central claim is an empirical observation, not a derivation: Section 8.1 reports measured task outcomes and explicitly says the QW-1 result is 'too coarse-grained' to conclude, and Section 7 disclaims statistical analysis. No prediction is computed from fitted inputs, no uniqueness theorem or ansatz is imported from the authors' prior work, and the self-citations (AutoProof [1,32], Design by Contract [20], Meyer's blog [21]) are background or tool references, not load-bearing. The main validity threats—small sample, all four no-shows from the AI group, no experience balancing—are internal-validity concerns, not circularity. The only mild self-referential element is the qualitative advice in Sections 9.2-9.3, induced and 'validated' on the same recorded sessions; this does not rise to equation-level circularity and does not affect the externally defined LLM vs no-LLM comparison.

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

The quantitative LLM versus no-LLM comparison rests mainly on the first four assumptions; the qualitative taxonomy rests on the fifth. None of these assumptions is benchmarked against an external reference.

assumptions (5)

domain assumption AutoProof with the supplied contracts is a valid ground truth for fix correctness in the tasks.
Section 5 describes verification as entirely static proof against contracts; if contracts are incomplete or tools unsound, the correctness labels could be wrong.
domain assumption The nine tasks and injected bugs are representative of real debugging scenarios.
Section 6 says tasks are drawn from tutorials, bug databases, and EiffelBase, but representativeness is not demonstrated.
domain assumption Random assignment with 25 participants and unbalanced no-shows yields comparable groups.
Section 6 reports four no-shows all from the AI group and no balancing by experience; the conclusion assumes this imbalance is ignorable.
domain assumption Participants followed instructions, including no hidden LLM use in the control group.
Section 6 asserts compliance based on examination of recordings, but social desirability could affect behavior in the AI group.
domain assumption Manual coding of video sessions for behavior patterns is reliable.
Section 9 derives patterns from manual review of 24 recordings, with no inter-rater reliability reported.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Do AI models help produce verified bug fixes?." pith.science (2026). https://pith.science/paper/GCTORMDD

@misc{pith2026250715822,
  author       = {Pith},
  title        = {Pith review of: Do AI models help produce verified bug fixes?},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/GCTORMDD}},
  note         = {Machine review of arXiv:2507.15822}
}

read the original abstract

Among areas of software engineering where AI techniques -- particularly, Large Language Models -- seem poised to yield dramatic improvements, an attractive candidate is Automatic Program Repair (APR), the production of satisfactory corrections to software bugs. Does this expectation materialize in practice? How do we find out, making sure that proposed corrections actually work? If programmers have access to LLMs, how do they actually use them to complement their own skills? To answer these questions, we took advantage of the availability of a program-proving environment, which formally determines the correctness of proposed fixes, to conduct a study of program debugging with two randomly assigned groups of programmers, one with access to LLMs and the other without, both validating their answers through the proof tools. The methodology relied on a division into general research questions (Goals in the Goal-Query-Metric approach), specific elements admitting specific answers (Queries), and measurements supporting these answers (Metrics). While applied so far to a limited sample size, the results are a first step towards delineating a proper role for AI and LLMs in providing guaranteed-correct fixes to program bugs. These results caused surprise as compared to what one might expect from the use of AI for debugging and APR. The contributions also include: a detailed methodology for experiments in the use of LLMs for debugging, which other projects can reuse; a fine-grain analysis of programmer behavior, made possible by the use of full-session recording; a definition of patterns of use of LLMs, with 7 distinct categories; and validated advice for getting the best of LLMs for debugging and Automatic Program Repair.

Figures

Figures reproduced from arXiv: 2507.15822 by the authors.

**Figure 1.** An AutoProof session • The Boogie prover [4, 17], itself relying on an SMT (Satisfiability Modulo Theory) solver, currently Z3 [9]. For each task in the experiment (see next section), the user is presented with a pre-filled program, which is valid Eiffel but buggy: clicking Verify will result in successful compilation but failed verification, with appropriate diagnostic such as a postcondition not being verified. … view at source ↗

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

36 extracted references · 34 canonical work pages

[1]

Web-based AutoProof installation, Anonymized

work page
[2]

AutoTest, https://www.eiﬀel.org/doc/eiﬀelstudio/U sing_AutoTest

work page
[3]

Proceedings of the ACM on Programming Languages 7(OOPSLA1), 85–111 (2023)

Barke, S., James, M.B., Polikarpova, N.: Grounded copil ot: How programmers interact with code-generating models. Proceedings of the ACM on Programming Languages 7(OOPSLA1), 85–111 (2023)

work page 2023
[4]

Barnett, M., Chang, B.Y.E., DeLine, R., Jacobs, B., Lein o, K.R.M.: Boogie: A Mod- ular Reusable Veriﬁer for Object-Oriented Programs. In: Int. Symposium on For- mal Methods for Components and Objects. pp. 364–387. Spring er (2005)

work page 2005
[5]

In: Marciniak, J.J

Basili, V.R., Caldiera, G., Rombach, H.D.: The goal ques tion metric approach. In: Marciniak, J.J. (ed.) Encyclopedia of Software Engineerin g, vol. 1, pp. 528–532. Wiley (1994)

work page 1994
[6]

arXiv preprint arXiv:2402.08147 (2024)

Brandfonbrener, D., Henniger, S., Raja, S., Prasad, T., Loughridge, C., Cassano, F., Hu, S.R., Yang, J., Byrd, W.E., Zinkov, R., et al.: Vermct s: Synthesizing multi- step programs using a veriﬁer, a large language model, and tr ee search. arXiv preprint arXiv:2402.08147 (2024)

arXiv 2024
[7]

Encyclopedia of software engineering 1(528-532), 6 (1994)

Caldiera, V.R.B.G., Rombach, H.D.: Goal question metri c paradigm. Encyclopedia of software engineering 1(528-532), 6 (1994)

work page 1994
[8]

Available at SSRN 4945566 (2024)

Cui, Z.K., Demirer, M., Jaﬀe, S., Musolﬀ, L., Peng, S., Salz, T.: The eﬀects of genera- tive ai on high skilled work: Evidence from three ﬁeld experiments with software developers. Available at SSRN 4945566 (2024)

work page 2024

Show all 36 references

[9]

In: I nternational Con- ference on Tools and Algorithms for the Construction and Ana lysis of Systems (TACAS)

De Moura, L., Bjørner, N.: Z3: An Eﬃcient SMT Solver. In: I nternational Con- ference on Tools and Algorithms for the Construction and Ana lysis of Systems (TACAS). pp. 337–340. Springer (2008)

2008
[10]

Doe, J.: Experiment bugs (07 2025), https://anonymous .4open.science/r/experiment_bugs-4385

2025
[11]

Doe, J.: Experiment bugs (07 2025), https://anonymous .4open.science/r/CodeForge-9ED8

2025
[12]

Doe, J.: Experiment instructions (07 2025), https://anonymous.4open.science/r/experiment_instructions-087E/

2025
[13]

In: EPIA Conference on Artiﬁcial Intelligence

Gonçalves, C.A., Gonçalves, C.T.: Assessment on the eﬀ ectiveness of github copi- lot as a code assistance tool: an empirical study. In: EPIA Conference on Artiﬁcial Intelligence. pp. 27–38. Springer (2024)

2024
[14]

In: Proceedings of the 23 rd Koli calling inter- national conference on computing education research

Kazemitabaar, M., Hou, X., Henley, A., Ericson, B.J., W eintrop, D., Grossman, T.: How novices use llm-based code generators to solve cs1 co ding tasks in a self-paced learning environment. In: Proceedings of the 23 rd Koli calling inter- national conference on computing educa...

2023
[15]

Personality and Social Psychology Review 2(3), 196–217 (1998)

Kerr, N.L.: Harking: Hypothesizing after the results a re known. Personality and Social Psychology Review 2(3), 196–217 (1998)

1998
[16]

Le Goues, C., Nguyen, T., Forrest, S., Weimer, W.: Genprog: A generic method for automatic software repair. Trans. on Software Engineering 38(1), 54–72 (2011)

2011
[17]

Leino, K.R.M., Rümmer, P.: The Boogie 2 Type Sys- tem: Design and Veriﬁcation Condition Generation, https://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.146.4277
[18]

arXiv preprint arXiv:2405.02580 (2024)

Liu, Y., Xue, Y., Wu, D., Sun, Y., Li, Y., Shi, M., Liu, Y.:Propertygpt: Llm-driven for- mal veriﬁcation of smart contracts through retrieval-augm ented property gen- eration. arXiv preprint arXiv:2405.02580 (2024)

2024 arXiv
[19]

ok pal, we have to code that now

Mailach, A., Gorgosch, D., Siegmund, N., Siegmund, J.: “ok pal, we have to code that now”: interaction patterns of programming beginners with a conversational chatbot. Empirical Software Engineering 30(1), 34 (2025)

2025
[20]

Design by Contract

Meyer, B.: Applying “Design by Contract”. Computer 25(10), 40–51 (1992)

1992
[21]

Blog article at Communications of the ACM (June 2023)

Meyer, B.: Ai does not help programmers. Blog article at Communications of the ACM (June 2023)

2023
[22]

ACM Computing Surveys (CSUR) 51(1), 1–24 (2018)

Monperrus, M.: Automatic software repair: A bibliogra phy. ACM Computing Surveys (CSUR) 51(1), 1–24 (2018)

2018
[23]

Monperrus, M.: The living review on automated program r epair. Ph.D. thesis, HAL Archives Ouvertes (2018)

2018
[24]

Nadella, S.: Microsoft ceo says up to 30% of the company’s code was written by ai (2025), https://techcrunch.com/2025/04/29/microsoft-ceo-say s-up-to-30-of-the-companys-code-was-written-by-ai/

2025
[25]

it’s weird that it knows what i want

Prather, J., Reeves, B.N., Denny, P., Becker, B.A., Lei nonen, J., Luxton-Reilly, A., Powell, G., Finnie-Ansley, J., Santos, E.A.: “it’s weird that it knows what i want”: Usability and interactions with copilot for novice program mers. ACM transac- tions on computer-human inte...

2023
[26]

LLM Debugging Study Questionnaire, https://forms.gl e/1kﬁPynkUdsvLfh6A
[27]

In: 2024 IEEE Frontiers in Education Conference (FIE)

Scholl, A., Kiesler, N.: How novice programmers use and experience chatgpt when solving programming exercises in an introductory cour se. In: 2024 IEEE Frontiers in Education Conference (FIE). pp. 1–9. IEEE (202 4)

2024
[28]

Communications of the ACM (July 2024), https://cacm.acm.org/news/the-impact-of-ai-on-compu ter-science-education/

Shein, E.: The impact of ai on computer science ed- ucation. Communications of the ACM (July 2024), https://cacm.acm.org/news/the-impact-of-ai-on-compu ter-science-education/

2024
[29]

Sun, C., Sheng, Y., Padon, O., Barrett, C.: Clover: Clos ed-loop veriﬁable code generation. In: Int. Symposium on AI Veriﬁcation. pp. 134–1 55. Springer (2024)

2024
[30]

arXiv preprint arXiv:2502.01573 (2025)

Teuber, S., Beckert, B.: Next steps in llm-supported ja va veriﬁcation. arXiv preprint arXiv:2502.01573 (2025)

2025 arXiv
[31]

arXiv preprint arXiv:2305

Tihanyi, N., Jain, R., Charalambous, Y., Ferrag, M.A., Sun, Y., Cordeiro, L.C.: A new era in software security: Towards self-healing softwar e via large language models and formal veriﬁcation. arXiv preprint arXiv:2305. 14752 (2023)

2023
[32]

In: I nternational Confer- ence on Tools and Algorithms for the Construction and Analys is of Systems (TACAS)

Tschannen, J., Furia, C.A., Nordio, M., Polikarpova, N .: AutoProof: Auto-active Functional Veriﬁcation of Object-Oriented Programs. In: I nternational Confer- ence on Tools and Algorithms for the Construction and Analys is of Systems (TACAS). pp. 566–580. Springer (2015)

2015
[33]

experience: Evaluat- ing the usability of code generation tools powered by large l anguage models

Vaithilingam, P., Zhang, T., Glassman, E.L.: Expectat ion vs. experience: Evaluat- ing the usability of code generation tools powered by large l anguage models. In: CHI conf. on human factors in computing systems (ext. abst.) . pp. 1–7 (2022)

2022
[34]

In: 2024 IEEE 48th Annual Computers, Software, and Applications Conference (COMPSAC)

Wang, W., Ning, H., Qian, S., Zhang, G., Wang, Y.: Charac terizing developers’ behaviors in llm-supported software development. In: 2024 IEEE 48th Annual Computers, Software, and Applications Conference (COMPSAC). pp. 1168–1177. IEEE (2024)

2024
[35]

I n: Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering

Wei, Y., Xia, C.S., Zhang, L.: Copiloting the copilots: Fusing large language mod- els with completion engines for automated program repair. I n: Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering...
[36]

In: Proceedings of t he 33rd ACM SIG- SOFT International Symposium on Software Testing and Analy sis

Xia, C.S., Zhang, L.: Automated program repair via conv ersation: Fixing 162 out of 337 bugs for $0.42 each using chatgpt. In: Proceedings of t he 33rd ACM SIG- SOFT International Symposium on Software Testing and Analy sis. pp. 819–831 (2024)

2024

Pith tools

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

[1] [1]

Web-based AutoProof installation, Anonymized

work page

[2] [2]

AutoTest, https://www.eiﬀel.org/doc/eiﬀelstudio/U sing_AutoTest

work page

[3] [3]

Proceedings of the ACM on Programming Languages 7(OOPSLA1), 85–111 (2023)

Barke, S., James, M.B., Polikarpova, N.: Grounded copil ot: How programmers interact with code-generating models. Proceedings of the ACM on Programming Languages 7(OOPSLA1), 85–111 (2023)

work page 2023

[4] [4]

Barnett, M., Chang, B.Y.E., DeLine, R., Jacobs, B., Lein o, K.R.M.: Boogie: A Mod- ular Reusable Veriﬁer for Object-Oriented Programs. In: Int. Symposium on For- mal Methods for Components and Objects. pp. 364–387. Spring er (2005)

work page 2005

[5] [5]

In: Marciniak, J.J

Basili, V.R., Caldiera, G., Rombach, H.D.: The goal ques tion metric approach. In: Marciniak, J.J. (ed.) Encyclopedia of Software Engineerin g, vol. 1, pp. 528–532. Wiley (1994)

work page 1994

[6] [6]

arXiv preprint arXiv:2402.08147 (2024)

Brandfonbrener, D., Henniger, S., Raja, S., Prasad, T., Loughridge, C., Cassano, F., Hu, S.R., Yang, J., Byrd, W.E., Zinkov, R., et al.: Vermct s: Synthesizing multi- step programs using a veriﬁer, a large language model, and tr ee search. arXiv preprint arXiv:2402.08147 (2024)

arXiv 2024

[7] [7]

Encyclopedia of software engineering 1(528-532), 6 (1994)

Caldiera, V.R.B.G., Rombach, H.D.: Goal question metri c paradigm. Encyclopedia of software engineering 1(528-532), 6 (1994)

work page 1994

[8] [8]

Available at SSRN 4945566 (2024)

Cui, Z.K., Demirer, M., Jaﬀe, S., Musolﬀ, L., Peng, S., Salz, T.: The eﬀects of genera- tive ai on high skilled work: Evidence from three ﬁeld experiments with software developers. Available at SSRN 4945566 (2024)

work page 2024