一句话：用等价性检查自动证明或反驳函数式编程作业的正确性，并通过函数归纳与聚类提升鲁棒性和可扩展性。
本文面向函数式编程课程中作业自动评分的需求，提出一种基于等价性检查的自动化正确性验证方法。系统输入学生提交与参考解答，通过程序等价性判定自动证明提交正确或给出反例。为适应真实课程中风格多样的程序，方法采用函数归纳处理递归、函数调用匹配处理辅助函数，从而提升鲁棒性；为应对数百份提交的规模，方法利用等价关系的传递性对学生提交进行聚类，发现可作为中间参考解的提交，从而提升可扩展性。作者在 Stainless 验证系统上实现了支持 Scala 程序等价性检查的原型，并在来自函数式编程课程及程序等价性检查文献的 4000 多个程序上进行了评估，这是目前该方向规模最大的评估。实验表明，系统能以高成功率生成归纳等价证明来证明程序正确，并对错误程序给出反例。
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. To be effective in the context of a real-world programming course, an automated grading system must be both robust, to support programs written in a variety of style, and scalable, to treat hundreds of submissions at once. 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 verification system, to support equivalence checking of Scala programs. We evaluate our system and its components on over 4000 programs drawn from a functional programming course and from the program equivalence checking literature; this is the largest such evaluation to date. We show that our system is capable of proving program correctness by generating inductive equivalence proofs, and providing counterexamples for incorrect programs, with a high success rate.
@article{paperbot1951,
title = {Proving and Disproving Equivalence of Functional Programming Assignments},
author = {Dragana Milovančević and Viktor Kunčak},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {PLDI},
year = {2023},
doi = {10.1145/3591258}
}