Research on program termination has a long tradition. However, most of the existing techniques target a single program only. We propose in this paper an incremental termination analysis approach by reusing certified modules across different program versions. A transformation-based procedure is further developed to increase the reusability of certified modules. The proposed approach has wide applicability, applicable to various program changes. The proposed technique, to the best of our knowledge, represents a novel attempt to the termination analysis of evolving programs. We implemented the approach on top of Ultimate Automizer. Experimental results show dramatic improvement of our approach over the state-of-the-art tool.
The artifact archive contains tool, source code, results and used benchmark programs in our evaluation. For details, please refer to README.md in the archive.
The full experimental results on artificial benchmarks and real-world benchmarks can be found in the following tables:
The artificial benchmarks and real-world benchmarks can be found in the following link: