Abstract
We present a method for constructing concrete executions or witnesses to abstract behavior specifications. The key concept is the use of an ordering on states which preserves containment of behaviors seen from the states. We present a modified depth-first search algorithm which uses the ordering to prune the requisite search paths and the memory needed for the history of the search. We apply the search to a model of a super-scalar pipeline.