We present an algorithm that uses decision procedures to generate finite-state abstractions of infinite-state systems. The algorithm compositionally abstracts the transitions of the system, relative to a given, fixed set of assertions. Thus, the number of validity checks is proportional to the number of transitions and their size, rather than the size of the abstract state-space. The generated abstractions are weakly preserving for Forall-CTL* temporal properties. We describe several applications of the algorithm, implemented using the decision procedures of the Stanford Temporal Prover (STeP).