Certification of compiler optimizations using kleene algebra with tests

Abstract

We use Kleene algebra with tests to verify a wide assort- ment of common compiler optimizations, including dead code elimina- tion, common subexpression elimination, copy propagation, loop hoist- ing, induction variable elimination, instruction scheduling, algebraic sim- plification, loop unrolling, elimination of redundant instructions, array bounds check elimination, and introduction of sentinels. In each of these cases, we give a formal equational proof of the correctness of the opti- mizing transformation.