一句话：提出基于符号执行与余归纳的演算，自动证明非严格函数式程序等价并生成反例。
程序等价性检查旨在确认两个程序在对应输入上具有相同行为。本文面向非严格（惰性）函数式语言，提出一个基于符号执行与余归纳（coinduction）的演算，用于检查程序等价性。该演算不仅能构造等价性证明，还能为不等价程序对推导出反例，包括由非终止行为引发的反例。作者进一步给出自动寻找等价证明与反例的方法，并实现工具 Nebula，用以证明 Haskell 程序的等价性。通过在已有基准性质集上应用 Nebula，作者展示了该工具在自动证明等价与自动生成反例两方面的实际有效性。
Program equivalence checking is the task of confirming that two programs have the same behavior on corresponding inputs. We develop a calculus based on symbolic execution and coinduction to check the equivalence of programs in a non-strict functional language. Additionally, we show that our calculus can be used to derive counterexamples for pairs of inequivalent programs, including counterexamples that arise from non-termination. We describe a fully automated approach for finding both equivalence proofs and counterexamples. Our implementation, Nebula, proves equivalences of programs written in Haskell. We demonstrate Nebula's practical effectiveness at both proving equivalence and producing counterexamples automatically by applying Nebula to existing benchmark properties.
@article{paperbot1471,
title = {Checking equivalence in a non-strict language},
author = {John C. Kolesar and Ruzica Piskac and William T. Hallahan},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {OOPSLA2},
year = {2022},
doi = {10.1145/3563340}
}