Program termination is a classic non-safety property that cannot in general be witnessed by a finite trace. This makes testing for non-termination challenging, and also makes it a natural target for symbolic proof. To confirm that non-termination is a practical and not theoretical problem, we provide a manual analysis of CVE’s due to non-termination, corresponding to security issues such as DoS vulnerabilities, finding 916 since 2000. Discovering non-termination is an under-approximate problem. We thus present UNTer, a sound and complete under-approximate logic for proving non-termination. We then extend UNTer with separation logic and develop UNTer$^{SL}$ for heap-manipulating programs. UNTer$^{SL}$ yields a compositional proof method amenable to automation via under-approximation and bi-abduction. We thus extend the Pulse analyser from Facebook and develop Pulse$^{\infty}$, an automated, compositional prover for non-termination based on UNTer$^{SL}$.