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 overapproximation 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 nontermination, it maintains of 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 te...

• Type: Journal
• Year: 2010
• Where: SAS
• Authors: William R. Harris, Akash Lal, Aditya V. Nori, Sriram K. Rajamani
• Keywords: Formal Methods, Loop, SAS 2010, Sequential Program, TREX