Compiler Optimization Correctness by Temporal Logic.

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

Higher Order and Symbolic Computation, 17 (3): 173-206, Kluwer, September, 2004.

PDF