Checking equivalence in a non-strict language

Abstract

Abstract 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.