Alternation for Termination

Proving termination of sequential programs is an important problem, both for establishing the total correctness of systems and as a component of proving more general termination and liveness properties. We present a new algorithm,

TRex

, that determines if a sequential program terminates on all inputs. The key characteristic of

TRex

is that it alternates between refining an over-approximation and an under-approximation of each loop in a sequential program. In order to prove termination,

TRex

maintains an over-approximation of the set of states that can be reached at the head of the loop. In order to prove non-termination, it maintains an under-approximation of the set of paths through the body of the loop. The over-approximation and under-approximation are used to refine each other iteratively, and help

TRex

to arrive quickly at a proof of either termination or non-termination.

TRex

refines the approximations in alternation by composing three different program analyses: (1) local termination provers that can quickly handle intricate loops, but not whole programs, (2) non-termination provers that analyze one cycle through a loop, but not all paths, and (3) global safety provers that can check safety properties of large programs, but cannot check liveness properties. This structure allows

TRex

to be instantiated using any of the pre-existing techniques for proving termination or non-termination of individual loops.

We evaluated

TRex

by applying it to prove termination or find bugs for a set of real-world programs and termination analysis benchmarks. Our results demonstrate that alternation allows

TRex

to prove termination or produce certified termination bugs more effectively than previous techniques.