Semantic program alignment for equivalence checking
Berkeley Churchill, Oded Padon, Rahul R. Sharma, Alex Aiken · 2019
We introduce a robust semantics-driven technique for program equivalence checking. Given two functions we find a trace alignment over a set of concrete executions of both programs and construct a product program particularly amenable to checking equivalence.