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.
CITATION STYLE
Kozen, D., & Patron, M. C. (2000). Certification of compiler optimizations using kleene algebra with tests. In Lecture Notes in Artificial Intelligence (Subseries of Lecture Notes in Computer Science) (Vol. 1861, pp. 568–582). Springer Verlag. https://doi.org/10.1007/3-540-44957-4_38
Mendeley helps you to discover research relevant for your work.