Jul 2026· ACM Transactions on Programming Languages and Systems· 0 citations· 83 references
TL;DR
This work was 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-output behaviour is identical.
Abstract
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 1700 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-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.
A comparative analysis of six LLMs for generating formative feedback on introductory Java programs containing predefined defects under controlled conditions reveals substantial cross-model variation, particularly in multi-defect scenarios.
Melina Najimi, Saba Yazdani, Marzieh Ahmadzadeh· Proceedings of the Canadian...· 0 citations
A framework for designing autograder test suites where a single programming problem is deconstructed into multiple competencies is introduced, supporting the instructor in designing a test suite aligned with the learning objectives related to the predefined competencies.
H. F. Guarilha, N. Arruda, Carla Delgado et al.· Anais do XXXIV Workshop sobr...· 0 citations
Findings indicate that behavioral signals present at the very start of an exercise contain useful clues about whether a student will ultimately solve the problem, and that keystroke-level editing logs provide additional value for early prioritization beyond execution logs alone.
This tutorial introduces a reusable, end-to-end evaluation pipeline grounded in empirical software engineering practices, focusing on post-generation validation rather than prompt design, allowing for validating AI-generated code in modern development workflows.
An algorithm and a prototype software system based on large language models are proposed to automate the creation and verification of unique assignments for laboratory work in information technology disciplines and makes it possible to significantly reduce instructors' time expenditure while preserving pedagogical cont...
O. D. Asenchik, A. A. Yastrebov, V. Ivashko· Bulletin Sukhoi State Techni...· 0 citations
Monty is presented: an autoformalization framework for assertions that tackles the challenges of expectations of validity of assertions and ambiguity in natural-language and produces the ground truth more reliably than when using LLMs naively to translate assertions.
