University of Minnesota
Software Engineering Center

You are here

Proving Correctness of Compiler Optimizations by Temporal Logic

Date of Publication: 
January 2002
Associated Research Groups: 
Publication Files: 
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'. The purpose of this paper is to show how such transformations may be proven correct. Our methodology is illustrated by three familiar optimizations, dead code elimination, constant folding and code motion. The meaning of correctness is that for any program π, if Rewrite ( π, π', p, I ⇒ I' φ ) then [[ π ]] ≡ [[ π' ]], i.e. π and π' have exactly the same semantics.
In Proc. of ACM POPL
@inproceedings{lacey02, author = "Lacey, D. and Jones, N. D. and Van Wyk, E. and Frederiksen, C. C.", title = "Proving Correctness of Compiler Optimizations by Temporal Logic", booktitle = "Proc. 29th ACM Symposium on Principles of Programming Languages", publisher = "Association of Computing Machinery", pages = "283--294", year = "2002"}