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 hav

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 http://en.wikipedia.org/wiki/Satisfiability_Modulo_Theories