Proving termination through conditional termination
Document typeConference report
Rights accessOpen Access
We present a constraint-based method for proving conditional termination of integer programs. Building on this, we construct a framework to prove (unconditional) program termination using a powerful mechanism to combine conditional termination proofs. Our key insight is that a conditional termination proof shows termination for a subset of program execution states which do not need to be considered in the remaining analysis. This facilitates more effective termination as well as non-termination analyses, and allows handling loops with different execution phases naturally. Moreover, our method can deal with sequences of loops compositionally. In an empirical evaluation, we show that our implementation VeryMax outperforms state-of-the-art tools on a range of standard benchmarks.
CitationBorralleras, C. [et al.]. Proving termination through conditional termination. A: International Conference on Tools and Algorithms for the Construction and Analysis of Systems. "Tools and Algorithms for the Construction and Analysis of Systems, 23rd International Conference, TACAS 2017: held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017: Uppsala, Sweden, April 22-29, 2017: proceedings, part I". Berlín: Springer, 2017, p. 99-117.
All rights reserved. This work is protected by the corresponding intellectual and industrial property rights. Without prejudice to any existing legal exemptions, reproduction, distribution, public communication or transformation of this work are prohibited without permission of the copyright holder