Skip to main content


eCommons@Cornell >
College of Engineering >
Computer Science >
Computer Science Technical Reports >

Please use this identifier to cite or link to this item:
Title: Certification of Compiler Optimizations using Kleene Algebra with Tests
Authors: Patron, Maria-Cristina
Kozen, Dexter
Keywords: computer science
technical report
Issue Date: Dec-1999
Publisher: Cornell University
Abstract: 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.
Appears in Collections:Computer Science Technical Reports

Files in This Item:

File Description SizeFormat
99-1779.pdf156.5 kBAdobe PDFView/Open
99-1779.ps154.48 kBPostscriptView/Open

Refworks Export

Items in eCommons are protected by copyright, with all rights reserved, unless otherwise indicated.


© 2014 Cornell University Library Contact Us