Compositional Termination Analysis

As a part of the project we worked on the problem of proving the termination of C programs. Modern termination provers rely on a safety checker to construct disjunctively well-founded transition invariants. This safety check is known to be the bottleneck of the procedure. We present an alternative algorithm that uses a light-weight check based on the transitivity of ranking relations to prove program termination. Experimental evaluation demonstrates that this algorithm is often able to conclude termination by examining only a small fraction of the program. As a consequence, our algorithm is able to outperform known approaches by multiple orders of magnitude.

More information is available at http://www.cprover.org/termination/

Also termination can be analyzed in context of loop summarization with appropriate abstract domains. Preliminary experimental results in this direction are available at the Loopfrog termination page. 

[1]

References