Automated Verification of Compiler Transformations