Semantic program alignment for equivalence checking

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.