Proving termination through conditional termination

View/Open
Cita com:
hdl:2117/179916
Document typeConference report
Defense date2017
PublisherSpringer
Rights accessOpen Access
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
ProjectAUTAR - A Unified Theory of Algorithmic Relaxations (EC-H2020-648276)
SOLUCIONES EFECTIVAS BASADAS EN LA LOGICA (MINECO-TIN2015-69175-C4-3-R)
SOLUCIONES EFECTIVAS BASADAS EN LA LOGICA (MINECO-TIN2015-69175-C4-3-R)
Abstract
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.
ISBN978-3-662-54577-5
Publisher versionhttps://link.springer.com/chapter/10.1007/978-3-662-54577-5_6
Files | Description | Size | Format | View |
---|---|---|---|---|
tacas17.pdf | 449,8Kb | View/Open |