Ir al contenido (pulsa Retorno)

Universitat Politècnica de Catalunya

    • Català
    • Castellano
    • English
    • LoginRegisterLog in (no UPC users)
  • mailContact Us
  • world English 
    • Català
    • Castellano
    • English
  • userLogin   
      LoginRegisterLog in (no UPC users)

UPCommons. Global access to UPC knowledge

Banner header
59.665 UPC E-Prints
You are here:
View Item 
  •   DSpace Home
  • E-prints
  • Departaments
  • Departament de Ciències de la Computació
  • Ponències/Comunicacions de congressos
  • View Item
  •   DSpace Home
  • E-prints
  • Departaments
  • Departament de Ciències de la Computació
  • Ponències/Comunicacions de congressos
  • View Item
JavaScript is disabled for your browser. Some features of this site may not work without it.

Proving termination through conditional termination

Thumbnail
View/Open
tacas17.pdf (449,8Kb)
Share:
 
 
10.1007/978-3-662-54577-5_6
 
  View Usage Statistics
Cita com:
hdl:2117/179916

Show full item record
Borralleras Andreu, Cristina
Brockschmidt, Marc
Larraz Hurtado, DanielMés informació
Oliveras Llunell, AlbertMés informacióMés informacióMés informació
Rodríguez Carbonell, EnricMés informacióMés informacióMés informació
Rubio Gimeno, AlbertoMés informacióMés informació
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)
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. 
URIhttp://hdl.handle.net/2117/179916
DOI10.1007/978-3-662-54577-5_6
ISBN978-3-662-54577-5
Publisher versionhttps://link.springer.com/chapter/10.1007/978-3-662-54577-5_6
Collections
  • Departament de Ciències de la Computació - Ponències/Comunicacions de congressos [1.231]
  • LOGPROG - Lògica i Programació - Ponències/Comunicacions de congressos [30]
Share:
 
  View Usage Statistics

Show full item record

FilesDescriptionSizeFormatView
tacas17.pdf449,8KbPDFView/Open

Browse

This CollectionBy Issue DateAuthorsOther contributionsTitlesSubjectsThis repositoryCommunities & CollectionsBy Issue DateAuthorsOther contributionsTitlesSubjects

© UPC Obrir en finestra nova . Servei de Biblioteques, Publicacions i Arxius

info.biblioteques@upc.edu

  • About This Repository
  • Contact Us
  • Send Feedback
  • Privacy Settings
  • Inici de la pàgina