Automated Induction for Proving Program Equivalence

Formal verification has made great advances in recent decades, resulting in tools that can verify strong correctness properties of important pieces of software infrastructure. In this thesis, we study a particular instance of formal verification: equivalence checking, and its applications in program verification. We propose a fully automated approach to equivalence checking that takes as input candidate programs and reference programs and uses functional induction to automatically prove or disprove the correctness of each candidate program. We next extend our approach to support equivalence checking of underspecified programs, and propose a new application of equivalence checking for measure transfer in termination proving. We implement our approach on top of the Stainless verifier to support equivalence checking of Scala programs. To evaluate our approach, we assemble data sets comprising a total of around 5000 Scala programs, drawn from equivalence checking benchmarks and programming assignments. Our evaluation and a case study show that our system outperforms state-of-the-art tools and is applicable to automated grading in undergraduate programming courses.