We propose an abstract interpretation algorithm for proving that a program terminates on all inputs.
The algorithm uses a novel abstract domain which uses ranking relations to conservatively represent
relations between intermediate program states. One of the attractive aspects of the algorithm is that
it abstracts information that is usually not important for proving termination such as program
invariants and yet it distinguishes between different reasons for termination which are not usually
maintained in existing abstract domains. We have implemented a prototype of the algorithm and shown
that in practice it is fast and precise.