Proving and Disproving Equivalence of Functional Programming Assignments

We present an automated approach to verify the correctness of programming assignments, such as the ones that arise in a functional programming course. Our approach takes as input student submissions and reference solutions, and uses equivalence checking to automatically prove or disprove correctness of each submission. We achieve robustness by handling recursion using functional induction and by handling auxiliary functions using function call matching. We achieve scalability using a clustering algorithm that leverages the transitivity of equivalence to discover intermediate reference solutions among student submissions. We implement our approach on top of the Stainless verifier, to support equivalence checking of Scala programs. Our results show that our system is capable of proving program correctness, as well as providing counterexamples in case of incorrect implementations, with a high success rate.

Dragana Milovančević is a PhD student in the LARA group at EPFL, under the supervision of Prof. Viktor Kunčak. Previously, she received her master’s degree from the University of Belgrade, where she was working as a teaching assistant. Her research interests are in the field of formal verification, where she applies equivalence checking to a variety of domains, including automated grading.