Formal Autograding in a Classroom (Experience Report)

We report our experience in enhancing automated grading in a functional programming course using formal verification. In our approach, we deploy a verifier for Scala programs to check equivalences between student submissions and reference solutions. Consequently, students receive more thorough evaluation of assignments that explores behaviours beyond those envisioned by tests or test generators. We collect student submissions and make them publicly available. We analyse the collected data set and find that we can use the conservative nature of our program equivalence checking as an advantage: we were able to use such equivalence to differentiate student solutions according to their high-level program structure, in particular their recursion pattern, even when their input-output behaviour is identical.