Patron, Maria-CristinaKozen, Dexter2007-04-232007-04-231999-12http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR99-1779https://hdl.handle.net/1813/7433We use Kleene algebra with tests to verify a wide assortment of common compiler optimizations, including dead code elimination, common subexpression elimination, copy propagation, loop hoisting, induction variable elimination, instruction scheduling, algebraic simplification, 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 optimizing transformation.160255 bytes158190 bytesapplication/pdfapplication/postscripten-UScomputer sciencetechnical reporttechnical report