コンパイラの最適化がプログラムの意味を変えず正しく動作することは非常に重要である．しかし，最適化には複雑なものも多く，コンパイラの最適化を正しく実装することは困難である．本論文では，プログラムが正しく最適化されたかどうかを時相論理を用いて最適化後に検査する手法を提案する．最適化によるプログラムの変形箇所が，プログラムの意味を変えないために満たすべき性質を時相論理で記述し，論理式で記述した性質を満たすかどうかを最適化後のプログラムをモデル検査することで検証する．この手法には，既存の複雑な最適化器にも適用でき，現実的な時間の範囲内での検査が可能であるといった利点がある．提案手法を実装し検査を実行した結果，COINSコンパイラの最適化器の未知のバグを発見することができた．