Automatic translation validation across the unoptimized
intermediate representation (IR) of the original source code
and the optimized executable assembly code is a desirable
capability, and has the potential to compete with existing approaches
to verified compilation such as CompCert.
A difficult subproblem is the automatic
identification of the correlations across the transitions between
the two programs' respective locations.
We present a counterexample-guided
algorithm to identify these correlations in a robust and
scalable manner. Our algorithm
has both theoretical and empirical advantages over prior work
in this problem space.