Staricka, Mathias2014-10-022014-10-022014-10-02https://hdl.handle.net/11299/166536Modern compilers perform many optimizations to code in order to increase its execution speed and e ciency. These optimizations generally involve a complex analysis of the program being compiled in order to determine where code can be optimized. The algorithms to perform these analyses are complex and can be di cult both to understand and to implement. In order to make the speci cation of these analyses simpler and easier to understand, we have developed a system for specifying optimizations using temporal logic. To perform these optimizations, we rst augment a language's attribute grammar speci cation to generate a control ow graph which has been annotated with predicates giving details necessary for the analysis. This control ow graph along with a temporal logic formula is provided as input to a model checker which determines which points in the program's control ow graph correspond with program statements that can be optimized. Finally, these statements are transformed accordingly to generate a new, optimized abstract syntax tree which can be used for code generation.en-USSumma Cum LaudeComputer ScienceCollege of Science and EngineeringThesis or Dissertation