Proving termination through conditional termination
| Autor: | Marc Brockschmidt, Enric Rodríguez-Carbonell, Daniel Larraz, Albert Rubio, Cristina Borralleras, Albert Oliveras |
|---|---|
| Přispěvatelé: | Universitat Politècnica de Catalunya. Departament de Ciències de la Computació, Universitat Politècnica de Catalunya. LOGPROG - Lògica i Programació |
| Jazyk: | angličtina |
| Rok vydání: | 2017 |
| Předmět: |
Theoretical computer science
Entry transition Termination proof Computer science Ranking function Program component Satisfiability modulo theory Program transformation 020207 software engineering Integer programming 02 engineering and technology Construct (python library) Mathematical proof Constraint (information theory) Range (mathematics) Informàtica::Informàtica teòrica [Àrees temàtiques de la UPC] 0202 electrical engineering electronic engineering information engineering Key (cryptography) 020201 artificial intelligence & image processing Programació en nombres enters Integer (computer science) |
| Zdroj: | UPCommons. Portal del coneixement obert de la UPC Universitat Politècnica de Catalunya (UPC) Tools and Algorithms for the Construction and Analysis of Systems ISBN: 9783662545768 TACAS (1) |
| DOI: | 10.1007/978-3-662-54577-5_6 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|