Afraid to change a running system? Using proven-correct transformation rules when their preconditions are satisfied, you don’t have to be :) In this talk, I present Abstract Execution, a specification and verification framework for properties of transformation rules on statement level. I demonstrate how to use my REFINITY workbench to model a refactoring technique called ‘Replace Exception with Test’, which generally will break your program when applied naively. Abstract Execution, the symbolic execution of abstract programs, has also been implied to prove the cost impact of transformations, and to restructure sequential code to prepare it for subsequent parallelization steps. Also these interesting applications are briefly presented.