Item
Ministerio de EconomÃa y Competitividad (Espanya)  
Albert, Elvira
Bofill Arasa, Miquel Borralleras, Cristina MartÃnMartÃn, Enrique Rubio, Albert 

When programs feature a complex control flow, existing techniques for resource analysis produce cost relation systems (CRS) whose cost functions retain the complex flow of the program and, consequently, might not be solvable into closedform upper bounds. This paper presents a novel approach to resource analysis that is driven by the result of a termination analysis. The fundamental idea is that the termination proof encapsulates the flows of the program which are relevant for the cost computation so that, by driving the generation of the CRS using the termination proof, we produce a linearlybounded CRS (LBCRS). A LBCRS is composed of cost functions that are guaranteed to be locally bounded by linear ranking functions and thus greatly simplify the process of CRS solving. We have built a new resource analysis tool, named MaxCore, that is guided by the VeryMax termination analyzer and uses CoFloCo and PUBS as CRS solvers. Our experimental results on the set of benchmarks from the Complexity and Termination Competition 2019 for C Integer programs show that MaxCore outperforms all other resource analysis tools This work was funded partially by the Spanish MICINN/FEDER, UE projects RTI2018094403BC31, RTI2018094403BC33 and RTI2018095609BI00, the MINECO project TIN201569175C42R, the MINECO/FEDER, UE projects TIN201569175C43R and TIN201566293R, and by the CM project S2018/TCS4314 

application/pdf  
http://hdl.handle.net/10256/18110  
eng  
Cambridge University Press (CUP)  
info:eurepo/semantics/altIdentifier/doi/10.1017/S1471068419000152 info:eurepo/semantics/altIdentifier/issn/14710684 info:eurepo/semantics/altIdentifier/eissn/14753081 info:eurepo/grantAgreement/MINECO//TIN201566293R/ES/LOGICA PARA PROBLEMAS COMBINATORIOS/ 

Tots els drets reservats  
ProgramaciÃ³ lÃ²gica
Logic programming ProgramaciÃ³ (MatemÃ tica) Programming (Mathematics) 

Resource Analysis driven by (Conditional) Termination Proofs  
info:eurepo/semantics/article  
DUGiDocs 