In this paper, we present a system that generates a Java optimizer from
specifications in temporal logic. The specification is simpler, and the
generated optimizers run more  efficiently than previously reported work.
We implemented a new model checker for a bidirectional CTL (computation
tree logic), a branching temporal logic. The model checker can check future and past
temporal CTL operators symmetrically without any conversion.
We also present a new specification language based on the bidirectional CTL
that can express typical optimization rules very naturally.
So far, a compiler optimizer using temporal logic was assumed to be impractical,
because it consumes too much time. However, with our method,
the generated Java compiler optimizer can compile all seven of the
SPECjvm98 benchmarks with a compile time from 15 seconds to 5 minutes.
We also gained insights into improving existing techniques for
decreasing the compilation time and expertise in specifying compiler
optimizations.