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.
Delivering high-quality formative feedback in large introductory programming courses remains challenging despite the widespread use of automated grading systems. Although large language models (LLMs) can generate natural-language explanations grounded in student code and test outcomes, their diagnostic reliability and pedagogical suitability require systematic evaluation. This study presents a comparative analysis of six LLMs for generating formative feedback on introductory Java programs containing predefined defects under controlled conditions. Model outputs were evaluated across key dimensions of feedback quality and performance. Results reveal substantial cross-model variation, particularly in multi-defect scenarios. More precise fault localization was associated with higher diagnostic accuracy and completeness, but also with more frequent instructional-constraint violations. No single model consistently outperformed others across all criteria, and response latency did not reliably correspond to diagnostic quality. These findings underscore the context-dependent nature of LLM-generated formative programming feedback.
Melina Najimi, Saba Yazdani, Marzieh Ahmadzadeh· Proceedings of the Canadian...· 0 citations
Automated programming autograders are essential for providing immediate feedback in programming education. However, conventional autograders are often limited to evaluating functional correctness through pass/fail tests. This article introduces a framework for designing autograder test suites where a single programming problem is deconstructed into multiple competencies. To automatically assign a grade to a student’s activity, the tool allows for defining weights for each test case, supporting the instructor in designing a test suite aligned with the learning objectives related to the predefined competencies. An experiment comparing this framework with traditional paper-based evaluations revealed a 97% reduction in grading time (r = 0.70 correlation), while effectively shifting the instructor’s role from grader to assessment designer.
H. F. Guarilha, N. Arruda, Carla Delgado et al.· Anais do XXXIV Workshop sobr...· 0 citations
This paper investigates the feasibility of early detection of struggling students during CS1 programming exercises using keystroke-level logs. Some students fail to reach a correct solution before the exercise ends, and by the time this becomes apparent from grades or final outcomes, the opportunity for timely instructor support aimed at helping them recover may have passed. We use data from the CodeBench platform, which records real-time code editing events at the keystroke level, alongside execution and submission logs. We define two outcome groups: Breakthrough (BT) students, whose prior submissions all receive 0% and whose final submission achieves full credit, and Fully Stuck (FS) students, whose submissions all receive 0% without reaching a correct solution. To examine this feasibility, we focus on two questions: (RQ1) whether adding keystroke-level editing features improves the prediction of FS students over execution-log features alone, and (RQ2) at which stage BT and FS students can be predicted most accurately. Experiments on the 2019-1 semester of the CodeBench dataset, comprising 507 students, compare three feature configurations: execution-based features (ExecOnly), CodeMirror-based features (CMOnly), and their combination (Combined). We evaluate prediction across successive submission-based stages during each exercise. In the earliest stage, CMOnly outperforms ExecOnly (AUROC 0.654 vs. 0.575), and Combined further improves over ExecOnly by +0.098 (AUROC 0.674). Across all configurations, the earliest stage yielded the strongest predictive signal. These 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.
Large Language Models (LLMs) are increasingly used to generate production code, yet systematic methods for evaluating their quality and security remain underdeveloped. 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. Participants will apply static analysis tools to assess maintainability, reliability, and security, and compare results across models, prompts, and human-written baselines. The pipeline supports structured aggregation and interpretation of outputs, enabling reproducible and defensible assessments. Extensions include agentic remediation, explainability for trust calibration, and bias-aware evaluation. Attendees will leave with practical evaluation artifacts and a principled framework 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. The solution is based on a three-agent pipeline that provides the generation of a reference master assignment, parametric variation of unique task instances, complexity control, and automatic error correction. An evaluation of the efficiency and correctness of the proposed solution was carried out. The testing results confirmed the high quality of the generated laboratory assignments and compliance with the requirements for the uniqueness of task variants. It was noted that the proposed solution makes it possible to significantly reduce instructors' time expenditure while preserving pedagogical control over the content of the educational process
O. D. Asenchik, A. A. Yastrebov, V. Ivashko· Bulletin Sukhoi State Techni...· 0 citations
Formal contracts are essential for software testing and verification, yet writing them remains labor-intensive and error-prone. LLMs offer a promising path toward autoformalization: synthesizing executable assertions from natural-language specifications and thereby bridging the gap between informal developer intent and formal executable specifications. We present Monty: an autoformalization framework for assertions that tackles the challenges of expectations of validity of assertions and ambiguity in natural-language. Our techniques are based on filtering formalizations using a novel conformance score metric and validity scores obtained from testing the code against formalized assertions. We evaluate our approach on 541 assertion-generation tasks derived from 22 collection-like Java classes, and show that our technique produces the ground truth more reliably (improving upto 20 points in precision on average) than when using LLMs naively to translate assertions.