一句话：将程序验证器用于本科编程课自动评分，通过等价性检查评估学生提交并区分递归结构。
本文报告在本科编程课程中利用形式验证增强自动评分的经验。传统测试评分难以确认解法正确性，也难以区分输入输出行为相同但结构不同的提交。作者在原有测试基础设施上部署程序验证器，将学生提交与参考解进行等价性检查，并分析 11 个练习的 1700 余份提交。结果显示，评分器能证明提交正确并给出反例；等价性检查还可识别高层程序结构，尤其是递归模式，即使行为相同。由此提高对惯用解法正确性的信心，并更全面刻画解法空间，发现教师未预见的解法。
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–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.
@article{paperbot3944,
title = {Formal Autograding in a Classroom (Extended Version)},
author = {Dragana Milovančević and Samuel Chassot and Mario Bucev and Marcin Wojnarowski and Viktor Kunčak},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {48},
number = {3},
year = {2026},
doi = {10.1145/3828727}
}