We establish principles for proving properties about infinite computations by reasoning about finite ones. We apply these principles to show that for a wide variety of verification problems - involving nondeterminism, fairness, and liveness - there are assertional verification methods that directly relate program and specification. Most previous research relies on transformations of programs in order to reduce a verification problem to problems that can be solved using classical techniques such a refinement mappings and well-founded orderings. Progress measures, the key innovation of this thesis, provide direct, syntax-independent verification techniques for a wide range of specifications. We exhibit progress measures for the language containment problem for nondeterministic automata; for verification with general fairness constraints; and for verification of very general specifications, including infinitary temporal logics. We obtain and optimal solution (in a recursion-theoretic sense) to the problem of verifying infinite computations by reasoning about finite ones. This result establishes a link between descriptive set theory and the theory of verification.