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 the context of loop summarization with appropriate abstract domains. Preliminary experimental results in this direction are available at the Loopfrog termination page


References

  1. Termination Analysis with Compositional Transition InvariantsKroening, D.; Sharygina, N.; Tsitovich, A.; Wintersteiger, C.M. , International Conference on Computer-Aided Verification (CAV), Edinburgh, UK, p.89-103, Springer (2010)