Shuvendu Lahiri, Rohit Sinha, and Chris Hawblitzel
Equivalence checking of imperative programs has several applications including compiler validation and cross-version verification. In this paper, we formalize a precise notion of it rootcause for a given counterexample to equivalence checking. Our notion of rootcause is inspired by work on program repair, but adapted to the case of two similar programs. By exploiting the semantic similarity between two programs, our formulation avoids the need for a template of fixes or the need for a complete repair to ensure equivalence, unlike existing works on program repair. We provide progressively weaker checks for detecting rootcauses that can be applicable even when multiple fixes are required to make the two programs equivalent. We provide optimizations based on Maximum Satisfiability (MAXSAT) and binary search to prune the space of candidate fixes. We have implemented the techniques and provide extensive evaluation on a set of real-world cross-version compiler validation benchmarks.