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.
Thu 8 DecDisplayed time zone: Auckland, Wellington change
15:30 - 17:00
|Checking Equivalence in a Non-strict Language|
|Necessity Specifications for Robustness|
Julian Mackay Victoria University of Wellington, Susan Eisenbach Imperial College London, James Noble Research & Programming, Sophia Drossopoulou Meta and Imperial College LondonDOI
|Quantitative strongest post: a calculus for reasoning about the flow of quantitative information|
Linpeng Zhang University College London, Benjamin Lucien Kaminski Saarland University and University College LondonDOI