I'm currently looking into the formalisation of limit-finding algorithms in a theorem prover, particularly exp-log-functions.
I found it very difficult to find information about what techniques modern CASs use for this. There is Dominik Gruntz's thesis and the book Symbolic Asymptotics by John Shackell – the idea in both cases seems to be to find an asymptotic expansion of the form
$$f(x) \sim \sum\limits_{i=0}^\infty c_i(x)\omega(x)^{e_i}$$
where the real exponents $e_i$ are strictly increasing and $\omega$ goes to $0$ very quickly in a way that dominates the $c_i$. Therefore, one can determine the limit by looking at the first term for which $c_i$ is non-zero. The approach works because constructing these asymptotic expansions is compositional.
My question is now: Is this still the state-of-the-art approach? Is it what real-life CASs actually use? Is there any more recent literature about these things?