Paper Accepted by FM 2024

Our paper has been accepted for presentation at FM 2024.

Our paper titled “Proving Functional Program Equivalence via Directed Lemma Synthesis” by Yican Sun (PKU), Ruyi Ji (PKU), Jian Fang (PKU), Xuanlin Jiang (PKU), Mingshuai Chen, and Yingfei Xiong (PKU) has been accepted for presentation at FM 2024 – the International Symposium on Formal Methods at Milan, Italy. This paper presents directed lemma synthesis, an effective approach to automating equivalence proofs for functional programs by discovering critical lemmas using program synthesis techniques.