Show simple item record

dc.contributor.authorBorralleras Andreu, Cristina
dc.contributor.authorBrockschmidt, Marc
dc.contributor.authorLarraz Hurtado, Daniel
dc.contributor.authorOliveras Llunell, Albert
dc.contributor.authorRodríguez Carbonell, Enric
dc.contributor.authorRubio Gimeno, Alberto
dc.contributor.otherUniversitat Politècnica de Catalunya. Departament de Ciències de la Computació
dc.date.accessioned2020-03-16T09:05:49Z
dc.date.available2020-03-16T09:05:49Z
dc.date.issued2017
dc.identifier.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.
dc.identifier.isbn978-3-662-54577-5
dc.identifier.urihttp://hdl.handle.net/2117/179916
dc.description.abstractWe 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.
dc.format.extent19 p.
dc.language.isoeng
dc.publisherSpringer
dc.subjectÀrees temàtiques de la UPC::Informàtica::Informàtica teòrica
dc.subject.lcshInteger programming
dc.subject.otherRanking function
dc.subject.otherEntry transition
dc.subject.otherProgram component
dc.subject.otherSatisfiability modulo theory
dc.subject.otherProgram transformation
dc.titleProving termination through conditional termination
dc.typeConference report
dc.subject.lemacProgramació en nombres enters
dc.contributor.groupUniversitat Politècnica de Catalunya. LOGPROG - Lògica i Programació
dc.identifier.doi10.1007/978-3-662-54577-5_6
dc.description.peerreviewedPeer Reviewed
dc.relation.publisherversionhttps://link.springer.com/chapter/10.1007/978-3-662-54577-5_6
dc.rights.accessOpen Access
local.identifier.drac27575419
dc.description.versionPostprint (author's final draft)
dc.relation.projectidinfo:eu-repo/grantAgreement/EC/H2020/648276/EU/A Unified Theory of Algorithmic Relaxations/AUTAR
dc.relation.projectidinfo:eu-repo/grantAgreement/MINECO/1PE/TIN2015-69175-C4-3-R
local.citation.authorBorralleras, C.; Brockschmidt, M.; Larraz, D.; Oliveras, A.; Rodríguez, E.; Rubio, A.
local.citation.contributorInternational Conference on Tools and Algorithms for the Construction and Analysis of Systems
local.citation.pubplaceBerlín
local.citation.publicationNameTools 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
local.citation.startingPage99
local.citation.endingPage117


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record

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