Certification of Compiler Optimizations using Kleene Algebra with Tests
| dc.contributor.author | Patron, Maria-Cristina | en_US |
| dc.contributor.author | Kozen, Dexter | en_US |
| dc.date.accessioned | 2007-04-23T18:19:41Z | |
| dc.date.available | 2007-04-23T18:19:41Z | |
| dc.date.issued | 1999-12 | en_US |
| dc.description.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. | en_US |
| dc.format.extent | 160255 bytes | |
| dc.format.extent | 158190 bytes | |
| dc.format.mimetype | application/pdf | |
| dc.format.mimetype | application/postscript | |
| dc.identifier.citation | http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR99-1779 | en_US |
| dc.identifier.uri | https://hdl.handle.net/1813/7433 | |
| dc.language.iso | en_US | en_US |
| dc.publisher | Cornell University | en_US |
| dc.subject | computer science | en_US |
| dc.subject | technical report | en_US |
| dc.title | Certification of Compiler Optimizations using Kleene Algebra with Tests | en_US |
| dc.type | technical report | en_US |