  We introduce skipping refinement, a new notion of correctness for reasoning
about optimized reactive systems. Reasoning about reactive systems using
refinement involves defining an abstract, high-level specification system and a
concrete, low-level implementation system. One then shows that every behavior
allowed by the implementation is also allowed by the specification. Due to the
difference in abstraction levels, it is often the case that the implementation
requires many steps to match one step of the specification, hence, it is quite
useful for refinement to directly account for stuttering. Some optimized
implementations, however, can actually take multiple specification steps at
once. For example, a memory controller can buffer the commands to the memory
and at a later time simultaneously update multiple memory locations, thereby
skipping several observable states of the abstract specification, which only
updates one memory location at a time. We introduce skipping simulation
refinement and provide a sound and complete characterization consisting of
"local" proof rules that are amenable to mechanization and automated
verification. We present case studies that highlight the applicability of
skipping refinement: a JVM-inspired stack machine, a simple memory controller
and a scalar to vector compiler transformation. Our experimental results
demonstrate that current model-checking and automated theorem proving tools
have difficultly automatically analyzing these systems using existing notions
of correctness, but they can analyze the systems if we use skipping refinement.
