Autograder for Functional Programming and Beyond - Dragana Milovancevic

In this talk, we present an automated approach for formally verifying the correctness of functional programming assignments. 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. We start by introducing our technique for automated equivalence checking, using the Stainless verification system. Our approach automatically matches function calls, generates proofs by induction, and checks them using SMT solvers. We then present our clustering algorithm that efficiently treats many programs at once. We conclude by demonstrating the effectiveness of our approach in practice, looking at various introductory Scala exercises.