Proving Correctness of Compiler Optimizations by Temporal Logic.

David Lacey and Neil D. Jones, Eric Van Wyk, and Carl C. Frederiksen,

Proceedings of 29th ACM Symposium on Principles of Programming Languages (POPL 2002), pp. 283-294, ACM, 2002.

PDF