CoChat
Sign Up
Cited by 33

Verifix: Verified Repair of Programming Assignments

Ahmed, Umair Z., Fan, Zhiyu, Yi, Jooyong, Al-Bataineh, Omar I., Roychoudhury, Abhik·2022·ACM Transactions on Software Engineering and Methodology
DOI 10.1145/3510418
Open this paper in CoChat — free account

Abstract

Automated feedback generation for introductory programming assignments is useful for programming education. Most works try to generate feedback to correct a student program by comparing its behavior with an instructor’s reference program on selected tests. In this work, our aim is to generate verifiably correct program repairs as student feedback. A student-submitted program is aligned and composed with a reference solution in terms of control flow, and the variables of the two programs are automatically aligned via predicates describing the relationship between the variables. When verification attempt for the obtained aligned program fails, we turn a verification problem into a MaxSMT problem whose solution leads to a minimal repair. We have conducted experiments on student assignments curated from a widely deployed intelligent tutoring system. Our results show that generating verified repair without sacrificing the overall repair rate is possible. In fact, our implementation, Verifix, is shown to outperform Clara, a state-of-the-art tool, in terms of repair rate. This shows the promise of using verified repair to generate high confidence feedback in programming pedagogy settings.

The claims and statistics of this paper haven’t been checked yet.

Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.

A few free checks a day · papers already verified open instantly · results are public

Integrity signals

Registry

Crossref · 10.1145/3510418

Cites

3 of 3 references verified0 citation errors · 0 not checkable

Statistics

Claims the paper makes

The claims and statistics of this paper haven’t been checked yet.

Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.

A few free checks a day · papers already verified open instantly · results are public

Claims other papers make about this one

Each is checked against this paper’s own text: does it say what the citing paper says it does?

  • Both VERIFIX and CLARA require an exact match between control flow graphs and a bijective relationship between variables; otherwise they return a structural mismatch error.

    “Both tools require an exact match between the control flow graphs (e.g., branches, loops) and a bijective relationship between the variables; otherwise, they return a structural mismatch error.”

    From Counterexample Guided Program Repair Using Zero-Shot Learning and MaxSAT-based Fault Localization (2025) · cites this paper as Ahmed et al. 2022

    Section 7 (Evaluation; page unavailable) explicitly distinguishes the tools: Clara requires matching control-flow edges, while Verifix requires matching CFA nodes and can repair some programs whose CFGs differ. Section 4.2 describes a bijective variable alignment for Verifix, but does not establish that Clara requires one. The paper reports structural-match failures, yet contradicts the claim that both tools require exact CFG matches. (LLM, conf=0.88)

    Checked by a reasoning model — may be wrong.

    Experimental — accuracy not yet measured

  • VERIFIX employs MaxSMT to align a buggy program with a reference implementation provided by the lecturer.

    “VERIFIX employs MaxSMT to align a buggy program with a reference implementation provided by the lecturer”

    From Counterexample Guided Program Repair Using Zero-Shot Learning and MaxSAT-based Fault Localization (2025) · cites this paper as Ahmed et al. 2022

  • Our method allows LLMs to repair more programs than other configurations and state-of-the-art symbolic program repair tools.

    “This method enables LLMS to repair more programs and produce superior fixes with smaller patches, outperforming both other configurations and state-of-the-art symbolic program repair tools (Gulwani, Radicek, and Zuleger 2018; Ahmed et al. 2022).”

    From Counterexample Guided Program Repair Using Zero-Shot Learning and MaxSAT-based Fault Localization (2025) · cites this paper as Ahmed et al. 2022

Self-check

Percentages, sums and reported differences re-computed from the paper’s own numbers.

The self-check needs the paper’s full text.

Cites

Flagged first, then by citations

Research works printed but not linked: 24

  1. Umair Z Ahmed, Pawan Kumar, Amey Karkare, Purushottam Kar, and Sumit Gulwani. 2018. Compilation error repair: for the student programs, from the student programs. In Proceedings of the 40th International Conference on Software Engineering: Software Engineering Education and Training. 78-87.
  2. Umair Z. Ahmed, Nisheeth Srivastava, Renuka Sindhgatta, and Amey Karkare. 2020. Characterizing the pedagogical benefits of adaptive feedback for compilation errors by novice programmers. In Proceedings of the ACM/IEEE 42nd International Conference on Software Engineering: Software Engineering Education and Training (ICSE). 139-150.
  3. Sahil Bhatia, Pushmeet Kohli, and Rishabh Singh. 2018. Neuro-symbolic program corrector for introductory program- ming assignments. In 2018 IEEE/ACM 40th International Conference on Software Engineering (ICSE). IEEE, 60-70.
  4. Darshak Chhatbar, Umair Z. Ahmed, and Purushottam Kar. 2020. MACER: A Modular Framework for Accelerated Compilation Error Repair. In International Conference on Artificial Intelligence in Education. Springer, 106-117.
  5. Stephen A Cook. 1978. Soundness and completeness of an axiom system for program verification. SIAM J. Comput. 7, 1 (1978), 70-90.
  6. Sumit Gulwani, Ivan Radicek, and Florian Zuleger. 2018. Automated clustering and program repair for introductory programming assignments. In Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). 465-480.
  7. Rahul Gupta, Soham Pal, Aditya Kanade, and Shirish Shevade. 2017. Deepfix: Fixing common c language errors by deep learning. In Conference on Artificial Intelligence (AAAI). 1345-1351.
  8. T.A. Henzinger, R Jhala, R Majumdar, and G Sutre. 2002. Lazy Abstraction. In ACM SIGPLAN SIGACT Symposium on Principles of Programming Languages (POPL).
  9. Yang Hu, Umair Z Ahmed, Sergey Mechtaev, Ben Leong, and Abhik Roychoudhury. 2019. Re-factoring based program repair applied to programming assignments. In Proceedings of the 34th IEEE/ACM International Conference on Automated Software Engineering (ASE). IEEE, 388-398.
  10. Shalini Kaleeswaran, Anirudh Santhiar, Aditya Kanade, and Sumit Gulwani. 2016. Semi-supervised verified feedback generation. In Proceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE). 739-750.
  11. Xuan-Bach D Le, Duc-Hiep Chu, David Lo, Claire Le Goues, and Willem Visser. 2017. S3: syntax-and semantic-guided repair synthesis via programming by examples. In Proceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering (FSE). 593-604.
  12. C. Le Goues, ThanhVu Nguyen, S. Forrest, and W. Weimer. 2012. GenProg: A Generic Method for Automatic Software Repair. IEEE Transactions on Software Engineering 38, 1 (Jan 2012), 54-72.
  13. Fan Long and Martin Rinard. 2016. Automatic patch generation by learning correct code. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). 298-312.
  14. Sergey Mechtaev, Manh-Dung Nguyen, Yannic Noller, Lars Grunske, and Abhik Roychoudhury. 2018. Semantic Program Repair Using a Reference Implementation. In Proceedings of the 40th International Conference on Software Engineering (ICSE).
  15. Sergey Mechtaev, Jooyong Yi, and Abhik Roychoudhury. 2016. Angelix: scalable multiline program patch synthesis via symbolic analysis. In Proceedings of the 38th International Conference on Software Engineering (ICSE). 691-701.
  16. Hoang Duong Thien Nguyen, Dawei Qi, Abhik Roychoudhury, and Satish Chandra. 2013. SemFix: program repair via semantic analysis. In Proceedings of the 35th International Conference on Software Engineering (ICSE). 772-781.
  17. Yewen Pu, Karthik Narasimhan, Armando Solar-Lezama, and Regina Barzilay. 2016. sk_𝑝: a neural program corrector for MOOCs. In Companion Proceedings of the 2016 ACM SIGPLAN International Conference on Systems, Programming, Languages and Applications: Software for Humanity. 39-40.
  18. Z Qi, F Long, S Achour, and M Rinard. 2015. An Analysis of Patch Plausibility and Correctness for Generate-and- Validate Patch Generation Systems. In Proceedings of the 2015 International Symposium on Software Testing and Analysis (ISSTA).
  19. Tyler J Ryan, Gene M Alarcon, Charles Walter, Rose Gamble, Sarah A Jessup, August Capiola, and Marc D Pfahler. 2019. Trust in automated software repair. In International Conference on Human-Computer Interaction. Springer, 452-470.
  20. Rishabh Singh, Sumit Gulwani, and Armando Solar-Lezama. 2013. Automated feedback generation for introductory programming assignments. In Proceedings of the 34th ACM SIGPLAN conference on Programming language design and implementation (PLDI). 15-26.
  21. Armando Solar-Lezama, Liviu Tancau, Rastislav Bodik, Sanjit Seshia, and Vijay Saraswat. 2006. Combinatorial sketching for finite programs. In Proceedings of the 12th international conference on Architectural support for programming languages and operating systems. 404-415.
  22. Ke Wang, Rishabh Singh, and Zhendong Su. 2017. Dynamic neural program embedding for program repair. arXiv preprint arXiv:1711.07163 (2017). · arXiv
  23. Ke Wang, Rishabh Singh, and Zhendong Su. 2018. Search, align, and repair: data-driven feedback generation for introductory programming exercises. In Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). 481-495.
  24. Jooyong Yi, Umair Z. Ahmed, Amey Karkare, Shin Hwei Tan, and Abhik Roychoudhury. 2017. A feasibility study of using automated program repair for introductory programming assignments. In Proceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering (FSE). 740-751.

Cited by

Sorted by citations

Authors
Ahmed, U. Z., Fan, Z., Yi, J., Al-Bataineh, O. I., & Roychoudhury, A.
Affiliations
  • National University of Singapore, Republic of Singapore
  • Ulsan National Institute of Science and Technology, South Korea
ORCID
Venue
ACM Transactions on Software Engineering and Methodology
Publisher
Association for Computing Machinery (ACM)
Published
2022-07-12
Volume
31
Issue
4
Pages
1-31
ISSN
  • 1049-331X
  • 1557-7392
DOI
10.1145/3510418
Cited by
33
References
3
Language
en
Licence
www.acm.org/publications/policies/copyright_policy#Background (vor)
Funders
  • Singapore Ministry of Education (MoE) Tier 3
  • National Research Foundation of Korea
  • Korea government (2021R1A2C1009819, 2021R1A5A1021944, 2021-0-01001)
  • Institute for Information & Communications Technology Planning & Evaluation

About these checks

Registry, retraction, Cites and statistics results are computed, not judged, with one exception: a printed reference that no index lists is read once by a model before it counts as a citation error. Claims are extracted by a model and kept only when their quote appears verbatim in the text; each cited source is then checked, with a model’s help, for whether it says what the claim relies on. Those verdicts can be wrong — read the claim’s quote and the cited source before relying on one.

Statistics and arithmetic are recomputed, not judged.

Confidence bands are shown only for fields calibrated on our annotated test set. None is calibrated yet, so no band is shown.

What counts as a claim ›How we measure confidence ›How we check this ›

Are you an author, or do you see a problem with this page? Request a review