Algebraic topology for termination proofs
As someone somewhat familiar with termination analysis, I'd say that the techniques are only as ad-hoc as the programs they aim to prove termination of, which is to say very ad-hoc indeed.
The crucial approach to scaling such analyses is modularity which allows decomposing the problem into sub-problems. Indeed this usually consists in identifying cycle-like things, typically either cycles in the control flow graph or the call graph, and decomposing it along it's strongly connected components (SCCs). We have very efficient algorithms to do this. No algebraic topology really required here AFAIK.
This is the easy part. The hard part is then identifying variants for each SCC. Here again you can do things in a modular manner, but it's more subtle. The most relevant fields as far as I can tell are constraint solving, and in particular linear programing and general combinatorial principles often related to Ramsey theory. Again, I'm not sure whether algebraic topology really has a role to play.

I will mention a connection between algebraic topology and rewrite theory though, if that can sate your curiosity: there is a strong analogy between homological algebra and confluence of rewrite systems. In particular, there is a connection between simply connected spaces, and (nice) rewrite systems in which every critical pair is closed (which implies confluence).
Here's some nice notes by Yves Guiraud, Eric Hoffbeck, and Philippe Malbos.
And Here's some really nice slides by Gershom Bazerman. Following the links to those papers should get you somewhere.