Formal Verification of a C-like Memory Model and Its Uses for Verifying Program Transformations