Translation and run-time validation of optimized code

The translation and run-time validation approaches of optimizing compilers are discussed. The translation validation approach performs a validation check after every run of the compiler, producing a formal proof that the target code is a correct implementation of the source code. A set of permutation rules is also described for more aggressive optimizations which, typically, alter the loop structure of the code, such as loop distribution and fusion, loop tiling, and lop interchanges. The run-time validation approach of speculative loop optimizations, that involves run-time tests, ensures the correctness of loop optimizations which neither the compiler nor compiler-validation techniques can guarantee the correctness.