On Proving and Disproving Equivalence of Functional Programming Assignments

We present an automated approach for verifying the correctness of programming assignments, such as ones arising in a functional programming course. Our approach takes a small set of reference implementations and a set of student implementations and checks, for each student implementation, whether it is provably correct. A function is considered correct if it is shown equivalent to a reference implementation either directly or indirectly through some other intermediate function. Equivalence checking automatically generates inductive proof attempts and checks them using function unfolding and SMT solving. We extend the Stainless verification system with our algorithm to support equivalence checking of functions written in Scala. We evaluate our system on submissions from a programming course. We show that our system is capable of proving function correctness by generating inductive equivalence proofs, as well as providing counterexamples in case of incorrect implementations, with a high success rate.