CS Talk
Dragana Milovančević
Host: Ruzica Piskac
Title: Proving Equivalence of Functional Programming Assignments
Abstract:
In this talk, 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 solutions and a set of student submissions and checks, for each submission, whether it is provably correct. A program is considered correct if it is shown equivalent to a reference solution either directly or indirectly through some other intermediate solution. We first show how equivalence checking automatically matches function calls, generates inductive proof attempts and checks them using function unfolding and SMT solving. We then demonstrate the effectiveness of our approach in practice, on programs drawn from a functional programming course and from the equivalence checking literature. Our results show that our system is capable of proving program correctness by generating inductive equivalence proofs, as well as providing counterexamples in case of incorrect implementations, with a high success rate.
Bio:
Dragana Milovančević is a PhD student in the LARA group at EPFL, under the supervision of 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.