Looking through the summary (and working from memories a while back, so I may be confusing stuff for this super optimizer with other super optimizers), they have a two step process for verification. For certain fixed inputs they check that the code outputs the same values (this can also be used as a hashing mechanism). Then afterwards they do symbolic comparison of the initial asm and the final asm, by converting each asm sequence into SMT[1] statements, feeding them the same input symbols and checking that their output symbols are the same. The tricky part here is doing the conversion as there are also many x86-64/SSE instructions; however, once you've done it you can just use an off-the-shelf solver.

This is why it is important that the code is loop free, because otherwise you couldn't use SMT and essentially would have to solve the halting problem. However, SMT, like SAT, is a NP-complete problem, but the good thing is that in most cases (according to the paper) solving the SMT problems generated is quick as they weren't designed to be diabolical.

[1] http://en.wikipedia.org/wiki/Satisfiability_Modulo_Theories

And SMT solvers pop up in another interesting paper! It's fascinating how over the last decade, I've started seeing SMT appear in practically anything and everything.

This is actually called 'verification', not validation [1].

[1]: http://en.wikipedia.org/wiki/Verification_and_validation_(so...

Section 5.2, Validation: "Code sequences are converted into SMT formulae ... and used to produce a query which asks whether both sequences produce the same side effects on live outputs when executed from the same initial machine state."