University of Minnesota
Software Engineering Center
/

You are here

Carl Christian Frederiksen

Recent Publications

Compiler Optimization Correctness by Temporal Logic

Rewrite rules with side conditions can elegantly express many classical compiler optimizations for imperative programming languages. In this paper, programs are written in an intermediate language and transformation-enabling side conditions are specified in a temporal logic suitable for describing program data flow.

Proving Correctness of Compiler Optimizations by Temporal Logic

Many classical compiler optimizations can be elegantly expressed using rewrite rules of form: II' if φ, where I, I' are intermediate language instructions and φ is a property expressed in a temporal logic suitable for describing program data flow. Its reading: If the current program π contains an instruction of form I at some control point p, and if flow condition φ is satisfied at p, then replace I by I'.