{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,14]],"date-time":"2026-01-14T22:58:59Z","timestamp":1768431539952,"version":"3.49.0"},"reference-count":37,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2022,7,12]],"date-time":"2022-07-12T00:00:00Z","timestamp":1657584000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Singapore Ministry of Education (MoE) Tier 3"},{"DOI":"10.13039\/501100003725","name":"National Research Foundation of Korea","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100003725","id-type":"DOI","asserted-by":"crossref"}]},{"name":"Korea government","award":["2021R1A2C1009819, 2021R1A5A1021944"],"award-info":[{"award-number":["2021R1A2C1009819, 2021R1A5A1021944"]}]},{"name":"Institute for Information & Communications Technology Planning & Evaluation"},{"name":"Korea government","award":["2021-0-01001"],"award-info":[{"award-number":["2021-0-01001"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Softw. Eng. Methodol."],"published-print":{"date-parts":[[2022,10,31]]},"abstract":"<jats:p>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\u2019s 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.<\/jats:p>","DOI":"10.1145\/3510418","type":"journal-article","created":{"date-parts":[[2022,3,28]],"date-time":"2022-03-28T11:51:53Z","timestamp":1648468313000},"page":"1-31","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":30,"title":["Verifix: Verified Repair of Programming\u00a0Assignments"],"prefix":"10.1145","volume":"31","author":[{"given":"Umair Z.","family":"Ahmed","sequence":"first","affiliation":[{"name":"National University of Singapore, Republic of Singapore"}]},{"given":"Zhiyu","family":"Fan","sequence":"additional","affiliation":[{"name":"National University of Singapore, Republic of Singapore"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7215-0855","authenticated-orcid":false,"given":"Jooyong","family":"Yi","sequence":"additional","affiliation":[{"name":"Ulsan National Institute of Science and Technology, South Korea"}]},{"given":"Omar I.","family":"Al-Bataineh","sequence":"additional","affiliation":[{"name":"National University of Singapore, Republic of Singapore"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7127-1137","authenticated-orcid":false,"given":"Abhik","family":"Roychoudhury","sequence":"additional","affiliation":[{"name":"National University of Singapore, Republic of Singapore"}]}],"member":"320","published-online":{"date-parts":[[2022,7,12]]},"reference":[{"key":"e_1_3_3_2_2","doi-asserted-by":"publisher","DOI":"10.1145\/3183377.3183383"},{"key":"e_1_3_3_3_2","doi-asserted-by":"publisher","DOI":"10.1145\/3377814.3381703"},{"key":"e_1_3_3_4_2","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"e_1_3_3_5_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-21437-0_17"},{"key":"e_1_3_3_6_2","doi-asserted-by":"publisher","DOI":"10.1145\/3180155.3180219"},{"key":"e_1_3_3_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-52237-7_9"},{"key":"e_1_3_3_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314596"},{"key":"e_1_3_3_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/3093336.3037754"},{"key":"e_1_3_3_10_2","doi-asserted-by":"publisher","DOI":"10.1137\/0207005"},{"key":"e_1_3_3_11_2","volume-title":"Proceedings of the 3rd International Workshop on Satisfiability Checking and Symbolic Computation (SC-square)","author":"Fontaine Pascal","year":"2018","unstructured":"Pascal Fontaine, Mizuhito Ogawa, Thomas Sturm, Xuan Tung Vu, et\u00a0al. 2018. Wrapping computer algebra is surprisingly successful for non-linear SMT. In Proceedings of the 3rd International Workshop on Satisfiability Checking and Symbolic Computation (SC-square)."},{"key":"e_1_3_3_12_2","article-title":"Automated program repair","volume":"62","author":"Goues Claire Le","year":"2019","unstructured":"Claire Le Goues, Michael Pradel, and Abhik Roychoudhury. 2019. Automated program repair. Commun. ACM 62, 12 (2019).","journal-title":"Commun. ACM"},{"key":"e_1_3_3_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/2635868.2635912"},{"key":"e_1_3_3_14_2","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192387"},{"key":"e_1_3_3_15_2","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v31i1.10742"},{"key":"e_1_3_3_16_2","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503279"},{"key":"e_1_3_3_17_2","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2019.00044"},{"key":"e_1_3_3_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/2950290.2950363"},{"key":"e_1_3_3_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/3106237.3106309"},{"key":"e_1_3_3_20_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2011.104"},{"key":"e_1_3_3_21_2","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837617"},{"key":"e_1_3_3_22_2","doi-asserted-by":"publisher","DOI":"10.1145\/3180155.3180247"},{"key":"e_1_3_3_23_2","doi-asserted-by":"publisher","DOI":"10.1145\/2884781.2884807"},{"key":"e_1_3_3_24_2","article-title":"Automatic software repair: A bibliography","volume":"51","author":"Monperrus Martin","year":"2018","unstructured":"Martin Monperrus. 2018. Automatic software repair: A bibliography. Comput. Surv. 51, 1 (2018).","journal-title":"Comput. Surv."},{"key":"e_1_3_3_25_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_3_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/349299.349314"},{"key":"e_1_3_3_27_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2013.6606623"},{"key":"e_1_3_3_28_2","first-page":"39","volume-title":"Proceedings of the ACM SIGPLAN International Conference on Systems, Programming, Languages and Applications: Software for Humanity","author":"Pu Yewen","year":"2016","unstructured":"Yewen Pu, Karthik Narasimhan, Armando Solar-Lezama, and Regina Barzilay. 2016. sk \\( \\_p \\) : A neural program corrector for MOOCs. In Proceedings of the ACM SIGPLAN International Conference on Systems, Programming, Languages and Applications: Software for Humanity. 39\u201340."},{"key":"e_1_3_3_29_2","doi-asserted-by":"publisher","DOI":"10.1145\/2771783.2771791"},{"key":"e_1_3_3_30_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-22351-9_31"},{"key":"e_1_3_3_31_2","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462195"},{"key":"e_1_3_3_32_2","doi-asserted-by":"publisher","DOI":"10.1145\/1168857.1168907"},{"key":"e_1_3_3_33_2","article-title":"Dynamic neural program embedding for program repair","author":"Wang Ke","year":"2017","unstructured":"Ke Wang, Rishabh Singh, and Zhendong Su. 2017. Dynamic neural program embedding for program repair. arXiv preprint arXiv:1711.07163 (2017).","journal-title":"arXiv preprint arXiv:1711.07163"},{"key":"e_1_3_3_34_2","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192384"},{"key":"e_1_3_3_35_2","doi-asserted-by":"publisher","DOI":"10.1145\/3106237.3106262"},{"key":"e_1_3_3_36_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10664-017-9552-y"},{"key":"e_1_3_3_37_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-68237-0_5"},{"key":"e_1_3_3_38_2","doi-asserted-by":"publisher","DOI":"10.1137\/0218082"}],"container-title":["ACM Transactions on Software Engineering and Methodology"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3510418","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3510418","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T18:09:45Z","timestamp":1750183785000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3510418"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,7,12]]},"references-count":37,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2022,10,31]]}},"alternative-id":["10.1145\/3510418"],"URL":"https:\/\/doi.org\/10.1145\/3510418","relation":{},"ISSN":["1049-331X","1557-7392"],"issn-type":[{"value":"1049-331X","type":"print"},{"value":"1557-7392","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,7,12]]},"assertion":[{"value":"2021-07-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-12-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2022-07-12","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}