Sciweavers

Share
CL
2000
Springer

Certification of Compiler Optimizations Using Kleene Algebra with Tests

11 years 5 months ago
Certification of Compiler Optimizations Using Kleene Algebra with Tests
We 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.
Dexter Kozen, Maria-Christina Patron
Added 24 Aug 2010
Updated 24 Aug 2010
Type Conference
Year 2000
Where CL
Authors Dexter Kozen, Maria-Christina Patron
Comments (0)
books