Verification of the correctness of compiler optimization using co-induction
M. Thiyagarajan, N. Sairam · Journal of Discrete Mathematical Sciences and Cryptography · 2007
We use co-algebraic theory of Kleene Algebra with Tests (KAT) to verify some common compiler optimizations including common sub-expression elimination, copy propagation, loop hoisting, induction variable elimination and loop unrolling. In each of these cases we give a co-inductive proof (using mixed automata) of the correctness of the optimizing transformation. We have also given a method for constructing a minimal mixed automata and a condition for proving the equivalence of two mixed automata.