{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,8]],"date-time":"2026-09-08T14:12:58Z","timestamp":1788876778731,"version":"build-2803163510"},"reference-count":88,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2026,9,8]],"date-time":"2026-09-08T00:00:00Z","timestamp":1788825600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"funder":[{"name":"DRIL funds from EPFL"},{"name":"UKRI Future Leaders Fellowship","award":["MR\/V024299\/1"],"award-info":[{"award-number":["MR\/V024299\/1"]}]},{"DOI":"10.13039\/501100001711","name":"Swiss National Science Foundation","doi-asserted-by":"crossref","award":["200021_219474"],"award-info":[{"award-number":["200021_219474"]}],"id":[{"id":"10.13039\/501100001711","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2026,9,30]]},"abstract":"<jats:p>We report our experience in enhancing automated grading in an undergraduate programming course using formal verification. In our experiments, we deploy a program verifier to check the equivalence between student submissions and our reference solutions, alongside the existing testing-based grading infrastructure. We collect and analyse over 1,700 student submissions to 11 programming exercises and show how our grader can prove submission correctness and report counterexamples. Beyond functional correctness, we were able to use the outcome of equivalence checks to differentiate student submissions according to their high-level program structure, in particular their recursion pattern, even when their input\u2013output 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.1145\/3828727","type":"journal-article","created":{"date-parts":[[2026,7,3]],"date-time":"2026-07-03T14:28:59Z","timestamp":1783088939000},"page":"1-26","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Formal Autograding in a Classroom (Extended Version)"],"prefix":"10.1145","volume":"48","author":[{"ORCID":"https:\/\/orcid.org\/0009-0003-0795-881X","authenticated-orcid":false,"given":"Dragana","family":"Milovan\u010devi\u0107","sequence":"first","affiliation":[{"name":"EPFL, Lausanne, Switzerland and Imperial College London, London, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-9751-9252","authenticated-orcid":false,"given":"Samuel","family":"Chassot","sequence":"additional","affiliation":[{"name":"EPFL, Lausanne, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0007-5317-5698","authenticated-orcid":false,"given":"Mario","family":"Bucev","sequence":"additional","affiliation":[{"name":"EPFL, Lausanne, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-7962-3904","authenticated-orcid":false,"given":"Marcin","family":"Wojnarowski","sequence":"additional","affiliation":[{"name":"EPFL, Lausanne, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7044-9522","authenticated-orcid":false,"given":"Viktor","family":"Kun\u010dak","sequence":"additional","affiliation":[{"name":"EPFL, Lausanne, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,9,8]]},"reference":[{"key":"e_1_3_4_2_2","doi-asserted-by":"crossref","first-page":"102","DOI":"10.1145\/3491140.3528282","volume-title":"Proceedings of the 9th ACM Conference on Learning @ Scale (L@S \u201922)","author":"Agarwal Nimisha","year":"2022","unstructured":"Nimisha Agarwal and Amey Karkare. 2022. LEGenT: Localizing errors and generating testcases for CS1. In Proceedings of the 9th ACM Conference on Learning @ Scale (L@S \u201922). ACM, 102\u2013112. DOI: 10.1145\/3491140.3528282"},{"issue":"3","key":"e_1_3_4_3_2","doi-asserted-by":"crossref","first-page":"489","DOI":"10.1145\/321765.321780","article-title":"Decidable properties of monadic functional schemas","volume":"20","author":"Ashcroft Edward","year":"1973","unstructured":"Edward Ashcroft, Zohar Manna, and Amir Pnueli. 1973. Decidable properties of monadic functional schemas. J. ACM 20, 3 (Jul. 1973), 489\u2013499.","journal-title":"J. ACM"},{"key":"e_1_3_4_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"e_1_3_4_5_2","volume-title":"4th Conference of the International Network for Didactic Research in University Mathematics (INDRUM \u201922)","author":"Bartzia Evmorfia","year":"2022","unstructured":"Evmorfia Bartzia, Antoine Meyer, and Julien Narboux. 2022. Proof assistants for undergraduate mathematics and computer science education: Elements of a priori analysis. In 4th Conference of the International Network for Didactic Research in University Mathematics (INDRUM \u201922). Reinhard Hochmuth, HAL, Hanovre, Germany. Retrieved from https:\/\/hal.science\/hal-03648357"},{"key":"e_1_3_4_6_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2004.09.013"},{"key":"e_1_3_4_7_2","first-page":"191","author":"Blanc R\u00e9gis William","year":"2017","unstructured":"R\u00e9gis William Blanc. 2017. Verification by Reduction to Functional Programs. 191","journal-title":"Verification by Reduction to Functional Programs"},{"key":"e_1_3_4_8_2","volume-title":"Scala Workshop","author":"William Blanc R\u00e9gis","year":"2013","unstructured":"R\u00e9gis William Blanc, Etienne Kneuss, Viktor Kuncak, and Philippe Suter. 2013. An overview of the Leon verification system: Verification by translation to recursive functions. In Scala Workshop. DOI: 10.1145\/2489837.2489838"},{"key":"e_1_3_4_9_2","unstructured":"Bolts. 2026. epfl-lara\/bolts. Retrieved from https:\/\/github.com\/epfl-lara\/bolts"},{"key":"e_1_3_4_10_2","volume-title":"Proceedings of the 52nd Annual Conference of SEFI","author":"Bovel Matt","year":"2024","unstructured":"Matt Bovel and Hamza Remmal. 2024. An automatic grading system for large classes. In Proceedings of the 52nd Annual Conference of SEFI. DOI: 10.5281\/zenodo.14256923"},{"key":"e_1_3_4_11_2","first-page":"343","volume-title":"Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design (FMCAD \u201922)","author":"Bucev Mario","year":"2022","unstructured":"Mario Bucev and Viktor Kun\u010dak. 2022. Formally verified quite OK image format. In Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design (FMCAD \u201922). TU Wien, 343\u2013348."},{"key":"e_1_3_4_12_2","unstructured":"Sergiu Bursuc Theodore Ehrenborg Shaowei Lin Lacramioara Astefanoaei Ionel Emilian Chiosa Jure Kukovec Alok Singh Oliver Butterley Adem Bizid Quinn Dougherty et al. 2025. A benchmark for vericoding: Formally verified program synthesis. arXiv:2509.22908. Retrieved from https:\/\/arxiv.org\/abs\/2509.22908"},{"key":"e_1_3_4_13_2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3110248","article-title":"Scaling up functional programming education: Under the hood of the OCaml MOOC","volume":"1","author":"Canou Benjamin","year":"2017","unstructured":"Benjamin Canou, Roberto Di Cosmo, and Gr\u00e9goire Henry. 2017. Scaling up functional programming education: Under the hood of the OCaml MOOC. Proc. ACM Program. Lang. 1, ICFP (2017), Article 4, 1\u201325.","journal-title":"Proc. ACM Program. Lang"},{"key":"e_1_3_4_14_2","doi-asserted-by":"crossref","unstructured":"Samuel Chassot and Viktor Kuncak. 2024. Verifying a realistic mutable hash table. arXiv:2107.08824. Retrieved from https:\/\/arxiv.org\/abs\/2107.08824","DOI":"10.1007\/978-3-031-63498-7_18"},{"key":"e_1_3_4_15_2","volume-title":"Proceedings of the 38th International Conference on Computer Aided Verification (CAV \u201926)","author":"ChassotKun\u010dak Samuel","year":"2026","unstructured":"Samuel ChassotKun\u010dak. 2026. Formally verified Linear-Time invertible lexing. In Proceedings of the 38th International Conference on Computer Aided Verification (CAV \u201926)."},{"key":"e_1_3_4_16_2","doi-asserted-by":"crossref","first-page":"104431","DOI":"10.1016\/j.compedu.2022.104431","article-title":"The role of feedback and guidance as intervention methods to foster computational thinking in educational robotics learning activities for primary school","volume":"180","author":"Chevalier Morgane","year":"2022","unstructured":"Morgane Chevalier, Christian Giang, Laila El-Hamamsy, Evgeniia Bonnet, Vaios Papaspyros, Jean-Philippe Pellet, Catherine Audrin, Margarida Romero, Bernard Baumberger, and Francesco Mondada. 2022. The role of feedback and guidance as intervention methods to foster computational thinking in educational robotics learning activities for primary school. Comput. Educ. 180 (2022), 104431.","journal-title":"Comput. Educ"},{"key":"e_1_3_4_17_2","first-page":"268","volume-title":"Proceedings of the 5th ACM SIGPLAN International Conference on Functional Programming (ICFP \u201900)","author":"Claessen Koen","year":"2000","unstructured":"Koen Claessen and John Hughes. 2000. QuickCheck: A lightweight tool for random testing of Haskell programs. In Proceedings of the 5th ACM SIGPLAN International Conference on Functional Programming (ICFP \u201900), 268\u2013279. DOI: 10.1145\/351240.351266"},{"key":"e_1_3_4_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/3428239"},{"key":"e_1_3_4_19_2","unstructured":"Lean Community. 2025. Functional Induction in Lean. Retrieved from https:\/\/leanprover-community.github.io\/mathlib4_docs\/Lean\/Meta\/Tactic\/FunInd.html"},{"key":"e_1_3_4_20_2","unstructured":"Scala Community. 2025. Variance in Scala. Retrieved from https:\/\/docs.scala-lang.org\/tour\/variances.html"},{"key":"e_1_3_4_21_2","doi-asserted-by":"crossref","first-page":"1177","DOI":"10.1145\/3408877.3432358","volume-title":"Proceedings of the 52nd ACM Technical Symposium on Computer Science Education (SIGCSE \u201921)","author":"Crichton Will","year":"2021","unstructured":"Will Crichton, Georgia Gabriela Sampaio, and Pat Hanrahan. 2021. Automating program structure classification. In Proceedings of the 52nd ACM Technical Symposium on Computer Science Education (SIGCSE \u201921), 1177\u20131183. DOI: 10.1145\/3408877.3432358"},{"key":"e_1_3_4_22_2","first-page":"337","volume-title":"Proceedings of the Theory and Practice of Software and 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS \u201908\/ETAPS \u201908)","author":"De Moura Leonardo","year":"2008","unstructured":"Leonardo De Moura and Nikolaj Bj\u00f8rner. 2008. Z3: An efficient SMT solver. In Proceedings of the Theory and Practice of Software and 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS \u201908\/ETAPS \u201908), 337\u2013340. DOI: 10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_4_23_2","doi-asserted-by":"publisher","DOI":"10.1145\/3670419"},{"key":"e_1_3_4_24_2","doi-asserted-by":"crossref","first-page":"349","DOI":"10.1145\/2642937.2642987","volume-title":"Proceedings of the 29th ACM\/IEEE International Conference on Automated Software Engineering (ASE \u201914)","author":"Felsing Dennis","year":"2014","unstructured":"Dennis Felsing, Sarah Grebing, Vladimir Klebanov, Philipp R\u00fcmmer, and Mattias Ulbrich. 2014. Automating regression verification. In Proceedings of the 29th ACM\/IEEE International Conference on Automated Software Engineering (ASE \u201914), 349\u2013360. DOI: 10.1145\/2642937.2642987"},{"issue":"2","key":"e_1_3_4_25_2","doi-asserted-by":"crossref","first-page":"159","DOI":"10.1017\/S0956796801004208","article-title":"DrScheme: A programming environment for scheme","volume":"12","author":"Findler Robert Bruce","year":"2002","unstructured":"Robert Bruce Findler, John Clements, Cormac Flanagan, Matthew Flatt, Shriram Krishnamurthi, Paul Steckler, and Matthias Felleisen. 2002. DrScheme: A programming environment for scheme. J. Funct. Program. 12, 2 (2002), 159\u2013182","journal-title":"J. Funct. Program"},{"key":"e_1_3_4_26_2","first-page":"35","volume-title":"Proceedings of the 10th Annual Conference on International Computing Education Research (ICER \u201914)","author":"Fisler Kathi","year":"2014","unstructured":"Kathi Fisler. 2014. The recurring rainfall problem. In Proceedings of the 10th Annual Conference on International Computing Education Research (ICER \u201914), 35\u201342. DOI: 10.1145\/2632320.2632346"},{"key":"e_1_3_4_27_2","first-page":"38","volume-title":"Proceedings of 16th Logical and Semantic Frameworks with Applications (Electronic Proceedings in Theoretical Computer Science, EPTCS)","author":"Halkj\u00e6r From Asta","year":"2022","unstructured":"Asta Halkj\u00e6r From, Frederik Krogsdal Jacobsen, and J\u00f8rgen Villadsen. 2022. 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), 38\u201355. DOI: 10.4204\/EPTCS.357.4"},{"key":"e_1_3_4_28_2","unstructured":"Sankalp Gambhir Simon Guilloud Dragana Milovan\u010devi\u0107 Philipp R\u00fcmmer and Viktor Kun\u010dak. 2023. LISA Tool Integration and Education Plans. Retrieved from https:\/\/aitp-conference.org\/2023\/abstract\/AITP_2023_paper_7.pdf"},{"key":"e_1_3_4_29_2","first-page":"750","volume-title":"Proceedings of the 54th ACM Technical Symposium on Computer Science Education (SIGCSE \u201923)","author":"Geng Chuqin","year":"2023","unstructured":"Chuqin Geng, Wenwen Xu, Yingjie Xu, Brigitte Pientka, and Xujie Si. 2023. 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 (SIGCSE \u201923), 750\u2013756. DOI: 10.1145\/3545945.3569882"},{"key":"e_1_3_4_30_2","doi-asserted-by":"publisher","DOI":"10.1007\/s40593-015-0080-x"},{"key":"e_1_3_4_31_2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/2699751","article-title":"OverCode: Visualizing variation in student solutions to programming problems at scale","volume":"7","author":"Glassman Elena L.","year":"2015","unstructured":"Elena L. Glassman, Jeremy Scott, Rishabh Singh, Philip J. Guo, and Robert C. Miller. 2015. OverCode: Visualizing variation in student solutions to programming problems at scale. ACM Trans. Comput.-Hum. Interact. 22, 2 (2015), 7:1\u20137:35.","journal-title":"ACM Trans. Comput.-Hum. Interact"},{"key":"e_1_3_4_32_2","doi-asserted-by":"crossref","first-page":"241","DOI":"10.1002\/stvr.1472","article-title":"Regression verification: Proving the equivalence of similar programs","author":"Godlin Benny","year":"2013","unstructured":"Benny Godlin and Ofer Strichman. 2013. Regression verification: Proving the equivalence of similar programs. Softw. Test. Verif. Reliab. 23 (2013), 241\u2013258.","journal-title":"Softw. Test. Verif. Reliab"},{"key":"e_1_3_4_33_2","first-page":"415","volume-title":"Proceedings of the 55th ACM Technical Symposium on Computer Science Education V. 1 (SIGCSE \u201924)","author":"Griswold William G.","year":"2024","unstructured":"William G. Griswold. 2024. Experience report: Meet the professor\u2014A large-course intervention for increasing rapport. In Proceedings of the 55th ACM Technical Symposium on Computer Science Education V. 1 (SIGCSE \u201924), 415\u2013421. DOI: 10.1145\/3626252.3630844"},{"key":"e_1_3_4_34_2","doi-asserted-by":"publisher","DOI":"10.3166\/tsi.24.1113-1138"},{"key":"e_1_3_4_35_2","doi-asserted-by":"crossref","first-page":"465","DOI":"10.1145\/3192366.3192387","volume-title":"Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI \u201918)","author":"Gulwani Sumit","year":"2018","unstructured":"Sumit Gulwani, Ivan Radi\u010dek, 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 \u201918), 465\u2013480. DOI: 10.1145\/3192366.3192387"},{"key":"e_1_3_4_36_2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3341719","article-title":"Teaching the art of functional programming using automated grading (experience report)","volume":"115","author":"Hameer Aliya","year":"2019","unstructured":"Aliya Hameer and Brigitte Pientka. 2019. Teaching the art of functional programming using automated grading (experience report). Proc. ACM Program. Lang. 3, ICFP (2019), Article 115, 1\u201315.","journal-title":"Proc. ACM Program. Lang"},{"key":"e_1_3_4_37_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-06773-0_21"},{"key":"e_1_3_4_38_2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3360592","article-title":"System FR: Formalized foundations for the stainless verifier","volume":"166","author":"Hamza Jad","year":"2019","unstructured":"Jad Hamza, Nicolas Voirol, and Viktor Kun\u010dak. 2019. System FR: Formalized foundations for the stainless verifier. Proc. ACM Program. Lang. 3, OOPSLA (2019), Article 166, 1\u201330.","journal-title":"Proc. ACM Program. Lang"},{"key":"e_1_3_4_39_2","first-page":"799","volume-title":"Proceedings of the 54th ACM Technical Symposium on Computer Science Education V. 1 (SIGCSE \u201923)","author":"Hart Rowan","year":"2023","unstructured":"Rowan Hart, Brian Hays, Connor McMillin, El Kindi Rezig, Gustavo Rodriguez-Rivera, and Jeffrey A. Turkstra. 2023. 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 (SIGCSE \u201923), 799\u2013805. DOI: 10.1145\/3545945.3569817"},{"key":"e_1_3_4_40_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-25379-9_16"},{"key":"e_1_3_4_41_2","unstructured":"INRIA. 2021. Functional Induction in Coq. Retrieved from https:\/\/coq.inria.fr\/refman\/using\/libraries\/funind.html"},{"key":"e_1_3_4_42_2","doi-asserted-by":"crossref","first-page":"63","DOI":"10.4204\/EPTCS.375.6","article-title":"On exams with the Isabelle proof assistant","volume":"03","author":"Jacobsen Frederik","year":"2023","unstructured":"Frederik Jacobsen and J\u00f8rgen Villadsen. 2023. On exams with the Isabelle proof assistant. Electron. Proc. Theor. Comput. Sci. 03 (2023), 63\u201376.","journal-title":"Electron. Proc. Theor. Comput. Sci"},{"issue":"301","key":"e_1_3_4_43_2","doi-asserted-by":"crossref","first-page":"236","DOI":"10.1080\/01621459.1963.10500845","article-title":"Hierarchical grouping to optimize an objective function","volume":"58","author":"Ward Joe H.","year":"1963","unstructured":"Joe H. Ward. Jr. 1963. Hierarchical grouping to optimize an objective function. J. Amer. Statist. Assoc. 58, 301 (1963), 236\u2013244.","journal-title":"J. Amer. Statist. Assoc"},{"key":"e_1_3_4_44_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-4449-4"},{"key":"e_1_3_4_45_2","first-page":"712","volume-title":"Proceedings of the 24th International Conference on Computer Aided Verification (CAV \u201912)","author":"Lahiri Shuvendu K.","year":"2012","unstructured":"Shuvendu K. Lahiri, Chris Hawblitzel, Ming Kawaguchi, and Henrique Reb\u00ealo. 2012. SYMDIFF: A language-agnostic semantic diff tool for imperative programs. In Proceedings of the 24th International Conference on Computer Aided Verification (CAV \u201912). Springer-Verlag, Berlin, 712\u2013717. DOI: 10.1007\/978-3-642-31424-7_54"},{"key":"e_1_3_4_46_2","unstructured":"LARA. 2023. Stainless. Retrieved from https:\/\/github.com\/epfl-lara\/stainless"},{"key":"e_1_3_4_47_2","unstructured":"EPFL LARA. 2025. Stainless. Retrieved from https:\/\/github.com\/epfl-lara\/inox\/"},{"key":"e_1_3_4_48_2","first-page":"1","article-title":"Automatic diagnosis and correction of logical errors for functional programming assignments","volume":"158","author":"Lee Junho","year":"2018","unstructured":"Junho Lee, Dowon Song, Sunbeom So, and Hakjoo Oh. 2018. Automatic diagnosis and correction of logical errors for functional programming assignments. Proc. ACM Program. Lang. 2, OOPSLA (2018), Article 158, 1\u201330.","journal-title":"Proc. ACM Program. Lang"},{"key":"e_1_3_4_49_2","first-page":"330","volume-title":"Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL \u201917)","author":"Madhavan Ravichandhran","year":"2017","unstructured":"Ravichandhran Madhavan, Sumith Kulal, and Viktor Kuncak. 2017. Contract-based resource verification for higher-order functions with memoization. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL \u201917). ACM, 330\u2013343. DOI: 10.1145\/3009837.3009874"},{"key":"e_1_3_4_50_2","first-page":"762","volume-title":"Proceedings of the 26th International Conference on Computer Aided Verification (CAV \u201914), Held as Part of the Vienna Summer of Logic (VSL \u201914)","volume":"8559","author":"Madhavan Ravichandhran","year":"2014","unstructured":"Ravichandhran Madhavan and Viktor Kuncak. 2014. Symbolic resource bound inference for functional programs. In Proceedings of the 26th International Conference on Computer Aided Verification (CAV \u201914), Held as Part of the Vienna Summer of Logic (VSL \u201914). Armin Biere and Roderick Bloem (Eds.), Lecture Notes in Computer Science, Vol. 8559, Springer, 762\u2013778. DOI: 10.1007\/978-3-319-08867-9_51"},{"key":"e_1_3_4_51_2","first-page":"701","volume-title":"Proceedings of the 57th ACM Technical Symposium on Computer Science Education V.1 (SIGCSE TS \u201926)","author":"Markova Anastasiya","year":"2026","unstructured":"Anastasiya Markova, Anish Kasam, Bryce Hackel, Marina Langlois, and Sam Lau. 2026. Designing and implementing skill tests at scale: Frequent, computer-based, proctored assessments with minimal infrastructure requirements. In Proceedings of the 57th ACM Technical Symposium on Computer Science Education V.1 (SIGCSE TS \u201926). ACM, New York, NY, 701\u2013707. DOI: 10.1145\/3770762.3772518"},{"key":"e_1_3_4_52_2","volume-title":"Teaching Logic Using a State-of-Art Proof Assistant","author":"Maxim Hendriks","year":"2010","unstructured":"Hendriks Maxim, Cezary Kaliszyk, Femke van Raamsdonk, and Freek Wiedijk. 2010. Teaching Logic Using a State-of-Art Proof Assistant. Acta Didactica Napocensia."},{"key":"e_1_3_4_53_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)72018-4"},{"issue":"1","key":"e_1_3_4_54_2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3636515","article-title":"Automated grading and feedback tools for programming education: A systematic review","volume":"24","author":"Messer Marcus","year":"2024","unstructured":"Marcus Messer, Neil C. C. Brown, Michael K\u00f6lling, and Miaojing Shi. 2024. Automated grading and feedback tools for programming education: A systematic review. ACM Trans. Comput. Educ. 24, 1 (2024), Article 10, 1\u201343.","journal-title":"ACM Trans. Comput. Educ"},{"key":"e_1_3_4_55_2","first-page":"256","volume-title":"ICSE Companion","author":"Miller Heather","year":"2014","unstructured":"Heather Miller, Philipp Haller, Lukas Rytz, and Martin Odersky. 2014. Functional programming for all! Scaling a MOOC for students and professionals alike. In ICSE Companion. ACM, 256\u2013263."},{"key":"e_1_3_4_56_2","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.17600207"},{"key":"e_1_3_4_57_2","author":"Milovancevic Dragana","year":"2023","unstructured":"Dragana Milovancevic and Viktor Kuncak. 2023. Proving and Disproving Equivalence of Functional Programming Assignments (Artifact).","journal-title":"Proving and Disproving Equivalence of Functional Programming Assignments (Artifact)"},{"key":"e_1_3_4_58_2","first-page":"1","article-title":"Proving and disproving equivalence of functional programming assignments","volume":"144","author":"Milovan\u010devi\u0107 Dragana","year":"2023","unstructured":"Dragana Milovan\u010devi\u0107 and Viktor Kun\u010dak. 2023. Proving and disproving equivalence of functional programming assignments. Proc. ACM Program. Lang., Article 144 (2023), 1\u201324.","journal-title":"Proc. ACM Program. Lang., Article"},{"key":"e_1_3_4_59_2","volume-title":"34th European Symposium on Programming on Programming Languages and Systems (ESOP \u201925), Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS","author":"Milovan\u010devi\u0107 Dragana","year":"2025","unstructured":"Dragana Milovan\u010devi\u0107, Mario Bucev, Marcin Wojnarowski, Samuel Chassot, and Viktor Kun\u010dak. 2025. Formal autograding in a classroom. In 34th European Symposium on Programming on Programming Languages and Systems (ESOP \u201925), Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS. Retrieved from https:\/\/infoscience.epfl.ch\/handle\/20.500.14299\/205841.2"},{"key":"e_1_3_4_60_2","author":"Milovan\u010devi\u0107 Dragana","year":"2025","unstructured":"Dragana Milovan\u010devi\u0107, Mario Bucev, Marcin Wojnarowski, Samuel Chassot, and Viktor Kun\u010dak. 2025. Formal Autograding in a Classroom (Artifact).","journal-title":"Formal Autograding in a Classroom (Artifact)"},{"key":"e_1_3_4_61_2","volume-title":"International Conference on Integrated Formal Methods (iFM)","author":"Milovan\u010devi\u0107 Dragana","year":"2024","unstructured":"Dragana Milovan\u010devi\u0107, Carsten Fuhs, Mario Bucev, and Viktor Kun\u010dak. 2024. Proving termination via measure transfer in equivalence checking. In International Conference on Integrated Formal Methods (iFM)."},{"key":"e_1_3_4_62_2","doi-asserted-by":"crossref","first-page":"252","DOI":"10.1145\/3132747.3132748","volume-title":"Proceedings of the 26th Symposium on Operating Systems Principles (SOSP \u201917)","author":"Nelson Luke","year":"2017","unstructured":"Luke Nelson, Helgi Sigurbjarnarson, Kaiyuan Zhang, Dylan Johnson, James Bornholt, Emina Torlak, and Xi Wang. 2017. Hyperkernel: Push-button verification of an OS kernel. In Proceedings of the 26th Symposium on Operating Systems Principles (SOSP \u201917). ACM, New York, NY, 252\u2013269. DOI: 10.1145\/3132747.3132748"},{"key":"e_1_3_4_63_2","doi-asserted-by":"crossref","first-page":"24","DOI":"10.1007\/978-3-642-27940-9_3","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"Nipkow Tobias","year":"2012","unstructured":"Tobias Nipkow. 2012. Teaching semantics with a proof assistant: No more LSD trip proofs. In Verification, Model Checking, and Abstract Interpretation. Viktor Kuncak and Andrey Rybalchenko (Eds.), Springer Berlin, Berlin, 24\u201338."},{"key":"e_1_3_4_64_2","unstructured":"Tobias Nipkow. 2022. Programming and Proving in Isabelle\/HOL. Retrieved from https:\/\/isabelle.in.tum.de\/dist\/Isabelle2022\/doc\/prog-prove.pdf"},{"key":"e_1_3_4_65_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9"},{"key":"e_1_3_4_66_2","first-page":"530","volume-title":"Proceedings of the 26th ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS \u201921)","author":"Oberhauser Jonas","year":"2021","unstructured":"Jonas Oberhauser, Rafael Lourenco de Lima Chehab, Diogo Behrens, Ming Fu, Antonio Paolillo, Lilith Oberhauser, Koustubha Bhat, Yuzhong Wen, Haibo Chen, Jaeho Kim, et al. 2021. 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 (ASPLOS \u201921). ACM, New York, NY, 530\u2013545. DOI: 10.1145\/3445814.3446748"},{"key":"e_1_3_4_67_2","unstructured":"Martin Odersky Lex Spoon and Bill Venners. 2019. Programming in Scala 4th Edition (A Comprehensive Step-by-Step Guide). Artima Sunnyvale CA. Retrieved from https:\/\/www.artima.com\/shop\/programming_in_scala_4ed"},{"key":"e_1_3_4_68_2","first-page":"1","volume-title":"30th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS \u201915)","author":"Ong Luke","year":"2015","unstructured":"Luke Ong. 2015. Higher-Order model checking: An overview. In 30th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS \u201915). IEEE Computer Society, 1\u201315. DOI: 10.1109\/LICS.2015.9"},{"key":"e_1_3_4_69_2","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1145\/1085114.1085123","volume-title":"Proceedings of the 2005 Workshop on Functional and Declarative Programming in Education (FDPE \u201905)","author":"Page Rex","year":"2005","unstructured":"Rex Page. 2005. Engineering software correctness. In Proceedings of the 2005 Workshop on Functional and Declarative Programming in Education (FDPE \u201905), 39\u201346. DOI: 10.1145\/1085114.1085123"},{"key":"e_1_3_4_70_2","first-page":"21","volume-title":"Proceedings of the 2008 International Workshop on Functional and Declarative Programming in Education (FDPE \u201908)","author":"Page Rex","year":"2008","unstructured":"Rex Page, Carl Eastlund, and Matthias Felleisen. 2008. Functional programming and theorem proving for undergraduates: A progress report. In Proceedings of the 2008 International Workshop on Functional and Declarative Programming in Education (FDPE \u201908), 21\u201330. DOI: 10.1145\/1411260.1411264"},{"key":"e_1_3_4_71_2","first-page":"370","volume-title":"Proceedings of the 16th International Conference on Educational Data Mining","author":"Phung Tung","year":"2023","unstructured":"Tung Phung, Jos\u00e9 Cambronero, Sumit Gulwani, Tobias Kohn, Rupak Majumdar, Adish Singla, and Gustavo Soares. 2023. Generating high-precision feedback for programming syntax errors using large language models. In Proceedings of the 16th International Conference on Educational Data Mining. International Educational Data Mining Society, Bengaluru, India, 370\u2013377. DOI: 10.5281\/zenodo.8115653"},{"key":"e_1_3_4_72_2","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1145\/1596550.1596552","volume-title":"Proceedings of the 14th ACM SIGPLAN International Conference on Functional Programming (ICFP \u201909)","author":"Pierce Benjamin C.","year":"2009","unstructured":"Benjamin C. Pierce. 2009. 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 (ICFP \u201909), 121\u2013122. DOI: 10.1145\/1596550.1596552"},{"key":"e_1_3_4_73_2","first-page":"39","volume-title":"Companion Proceedings of the 2016 ACM SIGPLAN International Conference on Systems, Programming, Languages and Applications: Software for Humanity (SPLASH Companion \u201916)","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 Companion Proceedings of the 2016 ACM SIGPLAN International Conference on Systems, Programming, Languages and Applications: Software for Humanity (SPLASH Companion \u201916), 39\u201340. DOI: 10.1145\/2984043.2989222"},{"key":"e_1_3_4_74_2","unstructured":"Pierre Rousselin. 2023. Mathematics with Coq for first-year undergraduate students. Retrieved from https:\/\/hal.science\/hal-04822929v1\/document"},{"key":"e_1_3_4_75_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-89439-1_20"},{"key":"e_1_3_4_76_2","doi-asserted-by":"crossref","first-page":"332","DOI":"10.1007\/978-3-030-94583-1_17","volume-title":"Proceedings of the 23rd International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI \u201922)","volume":"13182","author":"Schmid Georg Stefan","year":"2022","unstructured":"Georg Stefan Schmid and Viktor Kuncak. 2022. Generalized arrays for stainless frames. In Proceedings of the 23rd International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI \u201922). Bernd Finkbeiner and Thomas Wies (Eds.), Lecture Notes in Computer Science, Vol. 13182, Springer, 332\u2013354. DOI: 10.1007\/978-3-030-94583-1_17"},{"key":"e_1_3_4_77_2","first-page":"1258","volume-title":"Proceedings of the 55th ACM Technical Symposium on Computer Science Education V. 1 (SIGCSE \u201924)","author":"Singh Anjali","year":"2024","unstructured":"Anjali Singh, Anna Fariha, Christopher Brooks, Gustavo Soares, Austin Z. Henley, Ashish Tiwari, Chethan M. Heeryung Choi, and Sumit Gulwani. 2024. Investigating student mistakes in introductory data science programming. In Proceedings of the 55th ACM Technical Symposium on Computer Science Education V. 1 (SIGCSE \u201924), 1258\u20131264. DOI: 10.1145\/3626252.3630884"},{"key":"e_1_3_4_78_2","doi-asserted-by":"crossref","first-page":"15","DOI":"10.1145\/2499370.2462195","article-title":"Automated feedback generation for introductory programming assignments","volume":"48","author":"Singh Rishabh","year":"2013","unstructured":"Rishabh Singh, Sumit Gulwani, and Armando Solar-Lezama. 2013. Automated feedback generation for introductory programming assignments. SIGPLAN Not. 48 (2013), 15\u201326.","journal-title":"SIGPLAN Not"},{"key":"e_1_3_4_79_2","doi-asserted-by":"crossref","first-page":"850","DOI":"10.1145\/6592.6594","article-title":"Learning to program = Learning to construct mechanisms and explanations","volume":"29","author":"Soloway E.","year":"1986","unstructured":"E. Soloway. 1986. Learning to program = Learning to construct mechanisms and explanations. Commun. ACM. 29 (1986), 850\u2013858.","journal-title":"Commun. ACM"},{"key":"e_1_3_4_80_2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3360614","article-title":"Automatic and scalable detection of logical errors in functional programming assignments","volume":"3","author":"Song Dowon","year":"2019","unstructured":"Dowon Song, Myungho Lee, and Hakjoo Oh. 2019. Automatic and scalable detection of logical errors in functional programming assignments. Proc. ACM Program. Lang. 3, OOPSLA (2019), Article 188, 1\u201330.","journal-title":"Proc. ACM Program. Lang"},{"key":"e_1_3_4_81_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-23702-7_23"},{"key":"e_1_3_4_82_2","first-page":"641","volume-title":"Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI \u201922)","author":"Tao Runzhou","year":"2022","unstructured":"Runzhou Tao, Yunong Shi, Jianan Yao, Xupeng Li, Ali Javadi-Abhari, Andrew W. Cross, Frederic T. Chong, and Ronghui Gu. 2022. Giallar: Push-button verification for the qiskit quantum compiler. In Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI \u201922). ACM, New York, NY, 641\u2013656. DOI: 10.1145\/3519939.3523431"},{"key":"e_1_3_4_83_2","first-page":"107","volume-title":"Proceedings of the 6th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 \u201906)","author":"Vaillancourt Dale","year":"2006","unstructured":"Dale Vaillancourt, Rex Page, and Matthias Felleisen. 2006. ACL2 in DrScheme. In Proceedings of the 6th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 \u201906), 107\u2013116. DOI: 10.1145\/1217975.1217999"},{"key":"e_1_3_4_84_2","doi-asserted-by":"crossref","first-page":"18","DOI":"10.1145\/2774975.2774978","volume-title":"Proceedings of the 6th ACM SIGPLAN Symposium on Scala (SCALA \u201915)","author":"Voirol Nicolas","year":"2015","unstructured":"Nicolas Voirol, Etienne Kneuss, and Viktor Kuncak. 2015. Counter-example complete verification for higher-order functions. In Proceedings of the 6th ACM SIGPLAN Symposium on Scala (SCALA \u201915), 18\u201329. DOI: 10.1145\/2774975.2774978"},{"key":"e_1_3_4_85_2","doi-asserted-by":"crossref","first-page":"1004","DOI":"10.1016\/j.infsof.2012.12.005","article-title":"Software verification and graph similarity for automated evaluation of students\u2019 assignments","author":"Vujo\u0161evi\u0107-Jani\u010di\u0107 Milena","year":"2013","unstructured":"Milena Vujo\u0161evi\u0107-Jani\u010di\u0107, Mladen Nikoli\u0107, Du\u0161an To\u0161i\u0107, and Viktor Kuncak. 2013. Software verification and graph similarity for automated evaluation of students\u2019 assignments. Inf. Softw. Technol. 55 (2013), 1004\u20131016.","journal-title":"Inf. Softw. Technol"},{"key":"e_1_3_4_86_2","doi-asserted-by":"crossref","first-page":"481","DOI":"10.1145\/3192366.3192384","volume-title":"Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI \u201918)","author":"Wang Ke","year":"2018","unstructured":"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 \u201918). ACM, New York, NY, 481\u2013495. DOI: 10.1145\/3192366.3192384"},{"key":"e_1_3_4_87_2","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1145\/3230977.3230999","volume-title":"Proceedings of the 2018 ACM Conference on International Computing Education Research (ICER \u201918)","author":"Wrenn John","year":"2018","unstructured":"John Wrenn, Shriram Krishnamurthi, and Kathi Fisler. 2018. Who tests the testers? In Proceedings of the 2018 ACM Conference on International Computing Education Research (ICER \u201918). ACM, 51\u201359. DOI: 10.1145\/3230977.3230999"},{"key":"e_1_3_4_88_2","volume-title":"Proceedings of the 37th IEEE\/ACM International Conference on Automated Software Engineering (ASE)","author":"Zhang Jialu","year":"2023","unstructured":"Jialu Zhang, De Li, John Charles Kolesar, Hanyuan Shi, and Ruzica Piskac. 2023. Automated feedback generation for competition-level code. In Proceedings of the 37th IEEE\/ACM International Conference on Automated Software Engineering (ASE). DOI: 10.1145\/3551349.3560425"},{"key":"e_1_3_4_89_2","doi-asserted-by":"publisher","unstructured":"Craig Zilles Matthew West Geoffrey Herman and Timothy Bretl. 2019. Every University Should Have a Computer-Based Testing Facility. 414\u2013420. DOI: 10.5220\/0007753304140420","DOI":"10.5220\/0007753304140420"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3828727","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,9,8]],"date-time":"2026-09-08T14:05:58Z","timestamp":1788876358000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3828727"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,9,8]]},"references-count":88,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2026,9,30]]}},"alternative-id":["10.1145\/3828727"],"URL":"https:\/\/doi.org\/10.1145\/3828727","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,9,8]]},"assertion":[{"value":"2025-12-12","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-06-16","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-09-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}