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.

We demonstrate that our algorithm is applicable to challenging
equivalence problems beyond the scope of existing techniques. For
example, we verify the correctness of the hand-optimized vector
implementation of strlen that ships as part of the GNU C
Library, as well as the correctness of vectorization optimizations
for 56 benchmarks derived from the Test Suite for
Vectorizing Compilers.