形式化方法顶级会议 FM'24 近日公布论文录用名单，程序设计语言研究室的论文《Proving Functional Program Equivalence via Directed Lemma Synthesis》被该会议录用，详情如下。

标题：Proving Functional Program Equivalence via Directed Lemma Synthesis

作者：Yican Sun, Ruyi Ji, Jian Fang, Xuanlin Jiang, Mingshuai Chen, Yingfei Xiong

摘要：证明函数式程序的等价性是程序验证领域中一个基础的问题。该问题通常要求验证器对代数数据结构和结构递归函数的复合进行推理。现代程序验证器通过自动归纳的方法来解决该问题。然而，单凭自动归纳往往不够。此时需要验证器自己发现引理，证明引理并应用引理在证明原命题。但是，如何发现并应用引理缺乏系统的研究。本文提出了指向性引理合成，这个方法可以高效地找到证明函数式程序的等价性中需要的引理。本文首先整理了归纳友好的命题形式。这种形式能够保证归纳证明不会卡死。接着，我们提出了两种证明策略来合成引理，这些引理会将初始的命题反复转换，直至成为归纳友好的命题形式。两种证明策略都可以用程序合成器进行高效合成。我们的实验结果表明相比较于现有的基于枚举的引理合成方法，指向性引理合成可以节省 95.47%的运行时间并多解了38个问题。