This paper presents algorithms for program abstraction based on the principle of loop summarization, which, unlike traditional program approximation approaches (e.g., abstract interpretation), does not employ iterative ﬁxpoint computation, but instead computes symbolic abstract transformers with respect to a set of abstract domains. This allows for an eﬀective exploitation of problem speciﬁc abstract domains for summarization and, as a consequence, the precision of an abstract model may be tailored to speciﬁc veriﬁcation needs. Furthermore, we extend the concept of loop summarization to incorporate relational abstract domains to enable the discovery of transition invariants, which are subsequently used to prove termination of programs. Well-foundedness of the discovered transition invariants is ensured either by a separate decision procedure call or by using abstract domains that are well-founded by construction. We experimentally evaluate several abstract domains related to memory operations to detect buﬀer overﬂow problems. Also, our light-weight termination analysis is demonstrated to be eﬀective on a wide range of benchmarks, including OS device drivers.