We introduce refinement-based methods for analyzing the correctness of reactive systems. We propose skipping refinement, a new notion of refinement that extends the domain of applicability of refinement to include optimized reactive systems, systems that can run ``faster'' than their abstract high-level specifications. We develop a theory of skipping refinement and associated proof methods that are amenable to mechanized reasoning using existing verification tools. We also show that refinement can be used as part of an effective simulation-based testing methodology for reactive systems. We evaluate our work using several case studies.