In the talk I will present a series of abstractions that can be used to obtain approximated verification algorithms for parameterized systems with global conditions and different types of topology (ordered/unordered arrays, trees, graphs). The verification algorithms perform a symbolic exploration of a possibly infinite-state space and exploit the theory of well-quasi orderings for ensuring the theoretical termination of the analysis.