{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,7]],"date-time":"2025-05-07T04:14:40Z","timestamp":1746591280795,"version":"3.40.5"},"publisher-location":"Cham","reference-count":68,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031911200"},{"type":"electronic","value":"9783031911217"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T00:00:00Z","timestamp":1746057600000},"content-version":"vor","delay-in-days":120,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>We report our experience in enhancing automated grading in an undergraduate programming course using formal verification. In our experiment, we deploy a program verifier to check the equivalence between student submissions and our reference solutions, alongside the existing testing-based grading infrastructure. We were able to use program equivalence to differentiate student submissions according to their high-level program structure, in particular their recursion pattern, even when their input-output behaviour is identical. Consequently, we achieve (1) higher confidence in correctness of idiomatic solutions but also (2) more thorough assessment of solution landscape that reveals solutions beyond those envisioned by instructors.<\/jats:p>","DOI":"10.1007\/978-3-031-91121-7_7","type":"book-chapter","created":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T11:36:21Z","timestamp":1746185781000},"page":"154-174","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Formal Autograding in a Classroom"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0003-0795-881X","authenticated-orcid":false,"given":"Dragana","family":"Milovan\u010devi\u0107","sequence":"first","affiliation":[]},{"given":"Mario","family":"Bucev","sequence":"additional","affiliation":[]},{"given":"Marcin","family":"Wojnarowski","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0000-9751-9252","authenticated-orcid":false,"given":"Samuel","family":"Chassot","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7044-9522","authenticated-orcid":false,"given":"Viktor","family":"Kun\u010dak","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,5,1]]},"reference":[{"key":"7_CR1","doi-asserted-by":"publisher","unstructured":"Agarwal, N., Karkare, A.: LEGenT: Localizing Errors and Generating Testcases for CS1. In: Proceedings of the Ninth ACM Conference on Learning @ Scale. p. 102\u2013112. L@S\u201922, Association for Computing Machinery (2022). https:\/\/doi.org\/10.1145\/3491140.3528282","DOI":"10.1145\/3491140.3528282"},{"key":"7_CR2","doi-asserted-by":"publisher","unstructured":"Barbosa, H., Barrett, C., Brain, M., Kremer, G., Lachnitt, H., Mann, M., Mohamed, A., Mohamed, M., Niemetz, A., N\u00f6tzli, A., Ozdemir, A., Preiner, M., Reynolds, A., Sheng, Y., Tinelli, C., Zohar, Y.: cvc5: A Versatile and Industrial-Strength SMT Solver. In: Tools and Algorithms for the Construction and Analysis of Systems. pp. 415\u2013442 (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_24","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"7_CR3","unstructured":"Bartzia, E., Meyer, A., Narboux, J.: Proof assistants for undergraduate mathematics and computer science education: elements of a priori analysis. In: Trigueros, M. (ed.) INDRUM 2022: Fourth conference of the International Network for Didactic Research in University Mathematics. Reinhard Hochmuth, HAL, Hanovre, Germany (Oct 2022), https:\/\/hal.science\/hal-03648357"},{"key":"7_CR4","doi-asserted-by":"publisher","unstructured":"Bertot, Y., Guilhot, F., Pottier, L.: Visualizing Geometrical Statements with GeoView. Electr. Notes Theor. Comput. Sci. pp. 49\u201365 (11 2004). https:\/\/doi.org\/10.1016\/j.entcs.2004.09.013","DOI":"10.1016\/j.entcs.2004.09.013"},{"key":"7_CR5","doi-asserted-by":"publisher","unstructured":"Blanc, R.W., Kneuss, E., Kuncak, V., Suter, P.: An overview of the Leon verification system: Verification by translation to recursive functions. In: Scala Workshop (2013). https:\/\/doi.org\/10.1145\/2489837.2489838","DOI":"10.1145\/2489837.2489838"},{"key":"7_CR6","doi-asserted-by":"publisher","unstructured":"Blanc, R.W.: Verification by Reduction to Functional Programs p.\u00a0191 (2017). https:\/\/doi.org\/10.5075\/epfl-thesis-7636","DOI":"10.5075\/epfl-thesis-7636"},{"key":"7_CR7","doi-asserted-by":"publisher","unstructured":"Bovel, M., Remmal, H.: An automatic grading system for large classes. In: Proceedings of the 52nd Annual Conference of SEFI, Lausanne, Switzerland (2024). https:\/\/doi.org\/10.5281\/zenodo.14256923","DOI":"10.5281\/zenodo.14256923"},{"key":"7_CR8","doi-asserted-by":"publisher","unstructured":"Canou, B., Di\u00a0Cosmo, R., Henry, G.: Scaling up functional programming education: under the hood of the OCaml MOOC. Proc. ACM Program. Lang. 1(ICFP) (2017). https:\/\/doi.org\/10.1145\/3110248","DOI":"10.1145\/3110248"},{"key":"7_CR9","doi-asserted-by":"publisher","unstructured":"Chevalier, M., Giang, C., El-Hamamsy, L., Bonnet, E., Papaspyros, V., Pellet, J.P., Audrin, C., Romero, M., Baumberger, B., Mondada, F.: The role of feedback and guidance as intervention methods to foster computational thinking in educational robotics learning activities for primary school. Computers & Education 180, 104431 (2022). https:\/\/doi.org\/10.1016\/j.compedu.2022.104431","DOI":"10.1016\/j.compedu.2022.104431"},{"key":"7_CR10","doi-asserted-by":"publisher","unstructured":"Claessen, K., Hughes, J.: Quickcheck: a lightweight tool for random testing of Haskell programs. In: Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming. p. 268\u2013279. ICFP \u201900 (2000). https:\/\/doi.org\/10.1145\/351240.351266","DOI":"10.1145\/351240.351266"},{"key":"7_CR11","doi-asserted-by":"publisher","unstructured":"Clune, J., Ramamurthy, V., Martins, R., Acar, U.A.: Program Equivalence for Assisted Grading of Functional Programs. Proc. ACM Program. Lang. (OOPSLA) (2020). https:\/\/doi.org\/10.1145\/3428239","DOI":"10.1145\/3428239"},{"key":"7_CR12","doi-asserted-by":"publisher","unstructured":"Crichton, W., Sampaio, G.G., Hanrahan, P.: Automating Program Structure Classification. In: Proceedings of the 52nd ACM Technical Symposium on Computer Science Education. p. 1177\u20131183. SIGCSE \u201921 (2021). https:\/\/doi.org\/10.1145\/3408877.3432358","DOI":"10.1145\/3408877.3432358"},{"key":"7_CR13","doi-asserted-by":"crossref","unstructured":"De\u00a0Moura, L., Bj\u00f8rner, N.: Z3: An Efficient SMT Solver. In: Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. p. 337\u2013340. TACAS\u201908\/ETAPS\u201908 (2008), https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"7_CR14","doi-asserted-by":"publisher","unstructured":"Dongol, B., Dubois, C., Hallerstede, S., Hehner, E., Morgan, C., M\u00fcller, P., Ribeiro, L., Silva, A., Smith, G., de\u00a0Vink, E.: On Formal Methods Thinking in Computer Science Education. Form. Asp. Comput. (2024). https:\/\/doi.org\/10.1145\/3670419, https:\/\/doi.org\/10.1145\/3670419, just Accepted","DOI":"10.1145\/3670419"},{"key":"7_CR15","doi-asserted-by":"publisher","unstructured":"Felsing, D., Grebing, S., Klebanov, V., R\u00fcmmer, P., Ulbrich, M.: Automating Regression Verification. In: Proceedings of the 29th ACM\/IEEE International Conference on Automated Software Engineering. p. 349\u2013360. ASE \u201914 (2014). https:\/\/doi.org\/10.1145\/2642937.2642987","DOI":"10.1145\/2642937.2642987"},{"key":"7_CR16","doi-asserted-by":"publisher","unstructured":"Findler, R.B., Clements, J., Flanagan, C., Flatt, M., Krishnamurthi, S., Steckler, P., Felleisen, M.: DrScheme: a programming environment for Scheme. J. Funct. Program. p. 159\u2013182 (2002). https:\/\/doi.org\/10.1017\/S0956796801004208","DOI":"10.1017\/S0956796801004208"},{"key":"7_CR17","doi-asserted-by":"publisher","unstructured":"Fisler, K.: The recurring rainfall problem. In: Proceedings of the Tenth Annual Conference on International Computing Education Research. p. 35\u201342. ICER\u201914 (2014). https:\/\/doi.org\/10.1145\/2632320.2632346","DOI":"10.1145\/2632320.2632346"},{"key":"7_CR18","doi-asserted-by":"publisher","unstructured":"From, A., Jacobsen, F., Villadsen, J.: SeCaV: A sequent calculus verifier in Isabelle\/HOL. In: Proceedings of 16th Logical and Semantic Frameworks with Applications. Electronic Proceedings in Theoretical Computer Science, EPTCS, vol.\u00a0357, pp. 38\u201355 (2022). https:\/\/doi.org\/10.4204\/EPTCS.357.4","DOI":"10.4204\/EPTCS.357.4"},{"key":"7_CR19","unstructured":"Gambhir, S., Guilloud, S., Milovan\u010devi\u0107, D., R\u00fcmmer, P., Kun\u010dak, V.: Lisa tool integration and education plans (2023)"},{"key":"7_CR20","doi-asserted-by":"publisher","unstructured":"Geng, C., Xu, W., Xu, Y., Pientka, B., Si, X.: Identifying Different Student Clusters in Functional Programming Assignments: From Quick Learners to Struggling Students. In: Proceedings of the 54th ACM Technical Symposium on Computer Science Education. p. 750\u2013756. SIGCSE 2023 (2023). https:\/\/doi.org\/10.1145\/3545945.3569882","DOI":"10.1145\/3545945.3569882"},{"key":"7_CR21","doi-asserted-by":"publisher","unstructured":"Gerdes, A., Heeren, B., Jeuring, J., van Binsbergen, L.T.: Ask-Elle: an Adaptable Programming Tutor for Haskell Giving Automated Feedback. International Journal of Artificial Intelligence in Education (2016). https:\/\/doi.org\/10.1007\/s40593-015-0080-x","DOI":"10.1007\/s40593-015-0080-x"},{"key":"7_CR22","doi-asserted-by":"publisher","unstructured":"Glassman, E.L., Scott, J., Singh, R., Guo, P.J., Miller, R.C.: Overcode: Visualizing variation in student solutions to programming problems at scale. ACM Trans. Comput.-Hum. Interact. (2015). https:\/\/doi.org\/10.1145\/2699751, https:\/\/doi.org\/10.1145\/2699751","DOI":"10.1145\/2699751"},{"key":"7_CR23","doi-asserted-by":"publisher","unstructured":"Godlin, B., Strichman, O.: Regression verification: Proving the equivalence of similar programs. Software Testing Verification and Reliability pp. 241\u2013258 (2013). https:\/\/doi.org\/10.1002\/stvr.1472","DOI":"10.1002\/stvr.1472"},{"key":"7_CR24","doi-asserted-by":"publisher","unstructured":"Griswold, W.G.: Experience Report: Meet the Professor - A Large-Course Intervention for Increasing Rapport. In: Proceedings of the 55th ACM Technical Symposium on Computer Science Education V. 1. p. 415\u2013421. SIGCSE 2024 (2024). https:\/\/doi.org\/10.1145\/3626252.3630844","DOI":"10.1145\/3626252.3630844"},{"key":"7_CR25","doi-asserted-by":"publisher","unstructured":"Guilhot, F.: Formalisation en Coq et visualisation d\u2019un cours de g\u00e9om\u00e9trie pour le lyc\u00e9e. Technique et Science Informatiques pp. 1113\u20131138 (2005). https:\/\/doi.org\/10.3166\/tsi.24.1113-1138","DOI":"10.3166\/tsi.24.1113-1138"},{"key":"7_CR26","doi-asserted-by":"publisher","unstructured":"Gulwani, S., Radi\u010dek, I., Zuleger, F.: Automated clustering and program repair for introductory programming assignments. In: Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation. p. 465\u2013480. PLDI 2018 (2018). https:\/\/doi.org\/10.1145\/3192366.3192387, https:\/\/doi.org\/10.1145\/3192366.3192387","DOI":"10.1145\/3192366.3192387"},{"key":"7_CR27","doi-asserted-by":"publisher","unstructured":"Hameer, A., Pientka, B.: Teaching the art of functional programming using automated grading (experience report). ICFP (2019). https:\/\/doi.org\/10.1145\/3341719","DOI":"10.1145\/3341719"},{"key":"7_CR28","doi-asserted-by":"publisher","unstructured":"Hamza, J., Felix, S., Kun\u010dak, V., Nussbaumer, I., Schramka, F.: From Verified Scala to STIX File System Embedded Code Using Stainless. In: Deshmukh, J.V., Havelund, K., Perez, I. (eds.) NASA Formal Methods. pp. 393\u2013410. Springer International Publishing, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-06773-0_21","DOI":"10.1007\/978-3-031-06773-0_21"},{"key":"7_CR29","doi-asserted-by":"publisher","unstructured":"Hamza, J., Voirol, N., Kun\u010dak, V.: System FR: Formalized foundations for the Stainless verifier. OOPSLA, Association for Computing Machinery, New York, NY, USA (2019). https:\/\/doi.org\/10.1145\/3360592","DOI":"10.1145\/3360592"},{"key":"7_CR30","doi-asserted-by":"publisher","unstructured":"Hart, R., Hays, B., McMillin, C., Rezig, E.K., Rodriguez-Rivera, G., Turkstra, J.A.: Eastwood-Tidy: C Linting for Automated Code Style Assessment in Programming Courses. In: Proceedings of the 54th ACM Technical Symposium on Computer Science Education V. 1. p. 799\u2013805. SIGCSE 2023 (2023). https:\/\/doi.org\/10.1145\/3545945.3569817","DOI":"10.1145\/3545945.3569817"},{"key":"7_CR31","doi-asserted-by":"publisher","unstructured":"Henz, M., Hobor, A.: Teaching Experience: Logic and Formal Methods with Coq. In: Jouannaud, J.P., Shao, Z. (eds.) Certified Programs and Proofs. pp. 199\u2013215. Springer Berlin Heidelberg, Berlin, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-25379-9_16","DOI":"10.1007\/978-3-642-25379-9_16"},{"key":"7_CR32","unstructured":"INRIA: Functional Induction in Coq. https:\/\/coq.inria.fr\/refman\/using\/libraries\/funind.html (2021)"},{"key":"7_CR33","doi-asserted-by":"publisher","unstructured":"Jacobsen, F., Villadsen, J.: On exams with the isabelle proof assistant. Electronic Proceedings in Theoretical Computer Science pp. 63\u201376 (03 2023). https:\/\/doi.org\/10.4204\/EPTCS.375.6","DOI":"10.4204\/EPTCS.375.6"},{"key":"7_CR34","doi-asserted-by":"crossref","unstructured":"Kaufmann, M., Moore, J.S., Manolios, P.: Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, USA (2000), https:\/\/doi.org\/10.1007\/978-1-4615-4449-4","DOI":"10.1007\/978-1-4615-4449-4"},{"key":"7_CR35","doi-asserted-by":"publisher","unstructured":"Lahiri, S.K., Hawblitzel, C., Kawaguchi, M., Reb\u00ealo, H.: SYMDIFF: A Language-Agnostic Semantic Diff Tool for Imperative Programs. In: Proceedings of the 24th International Conference on Computer Aided Verification. p. 712\u2013717. CAV\u201912, Springer-Verlag, Berlin, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31424-7_54","DOI":"10.1007\/978-3-642-31424-7_54"},{"key":"7_CR36","unstructured":"LARA: Stainless. https:\/\/github.com\/epfl-lara\/stainless (2023)"},{"key":"7_CR37","doi-asserted-by":"publisher","unstructured":"Lee, J., Song, D., So, S., Oh, H.: Automatic Diagnosis and Correction of Logical Errors for Functional Programming Assignments. OOPSLA, Association for Computing Machinery, New York, NY, USA (2018). https:\/\/doi.org\/10.1145\/3276528","DOI":"10.1145\/3276528"},{"key":"7_CR38","unstructured":"Maxim, H., Kaliszyk, C., van Raamsdonk, F., Wiedijk, F.: Teaching logic using a state-of-art proof assistant. Acta Didactica Napocensia (2010)"},{"key":"7_CR39","doi-asserted-by":"publisher","unstructured":"McCarthy, J.: A basis for a mathematical theory of computation. In: Braffort, P., Hirschberg, D. (eds.) Computer Programming and Formal Systems, Studies in Logic and the Foundations of Mathematics, vol.\u00a035, pp. 33\u201370. Elsevier (1963). https:\/\/doi.org\/10.1016\/S0049-237X(08)72018-4","DOI":"10.1016\/S0049-237X(08)72018-4"},{"key":"7_CR40","doi-asserted-by":"publisher","unstructured":"Messer, M., Brown, N.C.C., K\u00f6lling, M., Shi, M.: Automated Grading and Feedback Tools for Programming Education: A Systematic Review. ACM Trans. Comput. Educ. 24(1) (2024). https:\/\/doi.org\/10.1145\/3636515","DOI":"10.1145\/3636515"},{"key":"7_CR41","doi-asserted-by":"crossref","unstructured":"Miller, H., Haller, P., Rytz, L., Odersky, M.: Functional programming for all! scaling a MOOC for students and professionals alike. In: ICSE Companion. pp. 256\u2013263. ACM (2014)","DOI":"10.1145\/2591062.2591161"},{"key":"7_CR42","doi-asserted-by":"publisher","unstructured":"Milovan\u010devi\u0107, D., Kun\u010dak, V.: Proving and Disproving Equivalence of Functional Programming Assignments. PLDI, Association for Computing Machinery, New York, NY, USA (2023). https:\/\/doi.org\/10.1145\/3591258","DOI":"10.1145\/3591258"},{"key":"7_CR43","doi-asserted-by":"publisher","unstructured":"Milovan\u010devi\u0107, D., Bucev, M., Wojnarowski, M., Chassot, S., Kun\u010dak, V.: Formal autograding in a classroom (artifact) (2025). https:\/\/doi.org\/10.5281\/zenodo.14624668","DOI":"10.5281\/zenodo.14624668"},{"key":"7_CR44","doi-asserted-by":"publisher","unstructured":"Nelson, L., Sigurbjarnarson, H., Zhang, K., Johnson, D., Bornholt, J., Torlak, E., Wang, X.: Hyperkernel: Push-Button Verification of an OS Kernel. In: Proceedings of the 26th Symposium on Operating Systems Principles. p. 252\u2013269. SOSP \u201917, Association for Computing Machinery, New York, NY, USA (2017). https:\/\/doi.org\/10.1145\/3132747.3132748","DOI":"10.1145\/3132747.3132748"},{"key":"7_CR45","doi-asserted-by":"crossref","unstructured":"Nipkow, T.: Teaching Semantics with a Proof Assistant: No More LSD Trip Proofs. In: Kuncak, V., Rybalchenko, A. (eds.) Verification, Model Checking, and Abstract Interpretation. pp. 24\u201338. Springer Berlin Heidelberg, Berlin, Heidelberg (2012)","DOI":"10.1007\/978-3-642-27940-9_3"},{"key":"7_CR46","unstructured":"Nipkow, T.: Programming and Proving in Isabelle\/HOL. https:\/\/isabelle.in.tum.de\/dist\/Isabelle2022\/doc\/prog-prove.pdf (2022)"},{"key":"7_CR47","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL: a proof assistant for higher-order logic, vol.\u00a02283. Springer Science & Business Media (2002), https:\/\/doi.org\/10.1007\/3-540-45949-9","DOI":"10.1007\/3-540-45949-9"},{"key":"7_CR48","doi-asserted-by":"publisher","unstructured":"Oberhauser, J., Chehab, R.L.d.L., Behrens, D., Fu, M., Paolillo, A., Oberhauser, L., Bhat, K., Wen, Y., Chen, H., Kim, J., Vafeiadis, V.: Vsync: push-button verification and optimization for synchronization primitives on weak memory models. In: Proceedings of the 26th ACM International Conference on Architectural Support for Programming Languages and Operating Systems. p. 530\u2013545. ASPLOS \u201921, Association for Computing Machinery, New York, NY, USA (2021). https:\/\/doi.org\/10.1145\/3445814.3446748","DOI":"10.1145\/3445814.3446748"},{"key":"7_CR49","unstructured":"Odersky, M., Spoon, L., Venners, B.: Programming in Scala, Fourth Edition (A comprehensive step-by-step guide). Artima, Sunnyvale, CA, USA (2019), https:\/\/www.artima.com\/shop\/programming_in_scala_4ed"},{"key":"7_CR50","doi-asserted-by":"publisher","unstructured":"Page, R.: Engineering software correctness. In: Proceedings of the 2005 Workshop on Functional and Declarative Programming in Education. p. 39\u201346. FDPE\u201905 (2005). https:\/\/doi.org\/10.1145\/1085114.1085123","DOI":"10.1145\/1085114.1085123"},{"key":"7_CR51","doi-asserted-by":"publisher","unstructured":"Page, R., Eastlund, C., Felleisen, M.: Functional programming and theorem proving for undergraduates: a progress report. In: Proceedings of the 2008 International Workshop on Functional and Declarative Programming in Education. p. 21\u201330. FDPE\u201908 (2008). https:\/\/doi.org\/10.1145\/1411260.1411264","DOI":"10.1145\/1411260.1411264"},{"key":"7_CR52","doi-asserted-by":"publisher","unstructured":"Pierce, B.C.: Lambda, the ultimate ta: using a proof assistant to teach programming language foundations. In: Proceedings of the 14th ACM SIGPLAN International Conference on Functional Programming. p. 121\u2013122. ICFP \u201909 (2009). https:\/\/doi.org\/10.1145\/1596550.1596552, https:\/\/doi.org\/10.1145\/1596550.1596552","DOI":"10.1145\/1596550.1596552"},{"key":"7_CR53","doi-asserted-by":"publisher","unstructured":"Pu, Y., Narasimhan, K., Solar-Lezama, A., Barzilay, R.: Sk_p: 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. p. 39\u201340. SPLASH Companion 2016 (2016). https:\/\/doi.org\/10.1145\/2984043.2989222","DOI":"10.1145\/2984043.2989222"},{"key":"7_CR54","unstructured":"Rousselin, P.: Mathematics with Coq for first-year undergraduate students (2023)"},{"key":"7_CR55","doi-asserted-by":"publisher","unstructured":"R\u00fcmmer, P.: A constraint sequent calculus for first-order logic with linear integer arithmetic. In: Logic for Programming, Artificial Intelligence, and Reasoning. pp. 274\u2013289 (2008). https:\/\/doi.org\/10.1007\/978-3-540-89439-1_20","DOI":"10.1007\/978-3-540-89439-1_20"},{"key":"7_CR56","doi-asserted-by":"publisher","unstructured":"Schmid, G.S., Kuncak, V.: Generalized arrays for stainless frames. In: Finkbeiner, B., Wies, T. (eds.) Verification, Model Checking, and Abstract Interpretation - 23rd International Conference, VMCAI 2022, Philadelphia, PA, USA, January 16-18, 2022, Proceedings. Lecture Notes in Computer Science, vol. 13182, pp. 332\u2013354. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-030-94583-1_17","DOI":"10.1007\/978-3-030-94583-1_17"},{"key":"7_CR57","doi-asserted-by":"publisher","unstructured":"Singh, A., Fariha, A., Brooks, C., Soares, G., Henley, A.Z., Tiwari, A., M, C., Choi, H., Gulwani, S.: Investigating student mistakes in introductory data science programming. In: Proceedings of the 55th ACM Technical Symposium on Computer Science Education V. 1. p. 1258\u20131264. SIGCSE 2024 (2024). https:\/\/doi.org\/10.1145\/3626252.3630884","DOI":"10.1145\/3626252.3630884"},{"key":"7_CR58","doi-asserted-by":"publisher","unstructured":"Singh, R., Gulwani, S., Solar-Lezama, A.: Automated feedback generation for introductory programming assignments. SIGPLAN Not. p. 15\u201326 (2013). https:\/\/doi.org\/10.1145\/2499370.2462195","DOI":"10.1145\/2499370.2462195"},{"key":"7_CR59","doi-asserted-by":"publisher","unstructured":"Soloway, E.: Learning to program = learning to construct mechanisms and explanations. Commun. ACM p. 850\u2013858 (1986). https:\/\/doi.org\/10.1145\/6592.6594","DOI":"10.1145\/6592.6594"},{"key":"7_CR60","doi-asserted-by":"publisher","unstructured":"Song, D., Lee, M., Oh, H.: Automatic and scalable detection of logical errors in functional programming assignments. OOPSLA, Association for Computing Machinery, New York, NY, USA (2019). https:\/\/doi.org\/10.1145\/3360614","DOI":"10.1145\/3360614"},{"key":"7_CR61","doi-asserted-by":"publisher","unstructured":"Suter, P., K\u00f6ksal, A.S., Kuncak, V.: Satisfiability modulo recursive programs. In: Yahav, E. (ed.) Static Analysis. pp. 298\u2013315 (2011). https:\/\/doi.org\/10.1007\/978-3-642-23702-7_23","DOI":"10.1007\/978-3-642-23702-7_23"},{"key":"7_CR62","doi-asserted-by":"publisher","unstructured":"Tao, R., Shi, Y., Yao, J., Li, X., Javadi-Abhari, A., Cross, A.W., Chong, F.T., Gu, R.: Giallar: push-button verification for the qiskit quantum compiler. In: Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation. p. 641\u2013656. PLDI 2022, Association for Computing Machinery, New York, NY, USA (2022). https:\/\/doi.org\/10.1145\/3519939.3523431","DOI":"10.1145\/3519939.3523431"},{"key":"7_CR63","doi-asserted-by":"publisher","unstructured":"Vaillancourt, D., Page, R., Felleisen, M.: ACL2 in DrScheme. In: Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and Its Applications. p. 107\u2013116. ACL2\u201906 (2006). https:\/\/doi.org\/10.1145\/1217975.1217999","DOI":"10.1145\/1217975.1217999"},{"key":"7_CR64","doi-asserted-by":"publisher","unstructured":"Voirol, N., Kneuss, E., Kuncak, V.: Counter-example complete verification for higher-order functions. In: Proceedings of the 6th ACM SIGPLAN Symposium on Scala. p. 18\u201329. SCALA 2015 (2015). https:\/\/doi.org\/10.1145\/2774975.2774978","DOI":"10.1145\/2774975.2774978"},{"key":"7_CR65","doi-asserted-by":"publisher","unstructured":"Vujo\u0161evi\u0107-Jani\u010di\u0107, M., Nikoli\u0107, M., To\u0161i\u0107, D., Kuncak, V.: Software verification and graph similarity for automated evaluation of students\u2019 assignments. Inf. Softw. Technol. p. 1004\u20131016 (2013). https:\/\/doi.org\/10.1016\/j.infsof.2012.12.005","DOI":"10.1016\/j.infsof.2012.12.005"},{"key":"7_CR66","doi-asserted-by":"publisher","unstructured":"Wang, K., Singh, R., Su, Z.: 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. p. 481\u2013495. PLDI 2018, Association for Computing Machinery, New York, NY, USA (2018). https:\/\/doi.org\/10.1145\/3192366.3192384","DOI":"10.1145\/3192366.3192384"},{"key":"7_CR67","doi-asserted-by":"publisher","unstructured":"Wrenn, J., Krishnamurthi, S., Fisler, K.: Who tests the testers? In: Proceedings of the 2018 ACM Conference on International Computing Education Research. p. 51\u201359. ICER\u201918, Association for Computing Machinery (2018). https:\/\/doi.org\/10.1145\/3230977.3230999","DOI":"10.1145\/3230977.3230999"},{"key":"7_CR68","doi-asserted-by":"publisher","unstructured":"Zhang, J., Li, D., Kolesar, J.C., Shi, H., Piskac, R.: Automated Feedback Generation for Competition-Level Code. In: Proceedings of the 37th IEEE\/ACM International Conference on Automated Software Engineering. ASE (2023). https:\/\/doi.org\/10.1145\/3551349.3560425, https:\/\/doi.org\/10.1145\/3551349.3560425","DOI":"10.1145\/3551349.3560425"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-91121-7_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,6]],"date-time":"2025-05-06T08:40:11Z","timestamp":1746520811000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-91121-7_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031911200","9783031911217"],"references-count":68,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-91121-7_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"1 May 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The complete data set from this paper is available in an open access Zenodo repository\u00a0[].","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Availability of Data and Software"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests."}},{"value":"ESOP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"European Symposium on Programming","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Hamilton, ON","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 May 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 May 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"34","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esop2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2025\/conferences\/esop\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}