Abstraction (in its various forms) is a powerful established technique in model-checking; still, when unbounded data-structures are concerned, it cannot always cope with divergence phenomena in a satisfactory way. Acceleration is an approach which is widely used to avoid divergence, but it has been applied mostly to integer programs. In this talk we will address the problem of accelerating transition relations for unbounded arrays. We will show how to compute accelerations in this domain; then we show how to adapt the so-called “monotonic abstraction” technique to efficiently handle complex formulae with nested quantifiers generated by the acceleration preprocessing. Notably, our technique can be easily plugged-in into abstraction/refinement loops, and strongly contributes to avoid divergence, as shown by experiments conducted with the MCMT model checker. This is a joint work with S. Ghilardi and N. Sharygina.