It is very important that compiler optimization works correctly without 
changing the semantics of a program. 
However, because there are many complex optimizations, it is generally 
difficult to implement them correctly.
In this paper, we propose a technique for testing whether or not the 
optimization transformations to the program have been performed 
correctly, by using temporal logic after the execution of the optimizer. 
We describe the properties that program points modified by the 
optimization have to satisfy to preserve the program semantics, 
in terms of temporal logic.
Then the system performs model checking on the optimized program,
to check if these program points satisfy the logical formulas .described.
This technique has the advantages that it can be applied to complex 
optimizers that already exist, and that checking occurs within a realistic time. 
We have implemented and executed this technique and found an unknown 
bug in an optimizer within a widely-used compiler.