{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T20:14:34Z","timestamp":1784837674418,"version":"3.55.0"},"reference-count":22,"publisher":"Cambridge University Press (CUP)","issue":"5-6","license":[{"start":{"date-parts":[[2019,9,20]],"date-time":"2019-09-20T00:00:00Z","timestamp":1568937600000},"content-version":"unspecified","delay-in-days":19,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theory and Practice of Logic Programming"],"published-print":{"date-parts":[[2019,9]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>When programs feature a complex control flow, existing techniques for resource analysis produce <jats:italic>cost relation systems<\/jats:italic> (CRS) whose cost functions retain the complex flow of the program and, consequently, might not be solvable into closed-form <jats:italic>upper bounds<\/jats:italic>. 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 <jats:italic>linearly-bounded<\/jats:italic> CRS (LB-CRS). A LB-CRS is composed of cost functions that are guaranteed to be <jats:italic>locally<\/jats:italic> 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.<\/jats:p>","DOI":"10.1017\/s1471068419000152","type":"journal-article","created":{"date-parts":[[2019,9,20]],"date-time":"2019-09-20T09:06:21Z","timestamp":1568970381000},"page":"722-739","source":"Crossref","is-referenced-by-count":12,"title":["Resource Analysis driven by (Conditional) Termination Proofs"],"prefix":"10.1017","volume":"19","author":[{"given":"ELVIRA","family":"ALBERT","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"MIQUEL","family":"BOFILL","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"CRISTINA","family":"BORRALLERAS","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1664-018X","authenticated-orcid":false,"given":"ENRIQUE","family":"MARTIN-MARTIN","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"ALBERT","family":"RUBIO","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2019,9,20]]},"reference":[{"key":"S1471068419000152_ref21","first-page":"8:1","article-title":"A termination analyzer for java bytecode based on path-length","volume":"3","author":"Spoto","year":"2010","journal-title":"ACM Trans. Program. Lang. Syst. 32"},{"key":"S1471068419000152_ref20","first-page":"745","volume-title":"Proc. CAV 2014","volume":"8559","author":"Sinn","year":"2014"},{"key":"S1471068419000152_ref15","doi-asserted-by":"crossref","first-page":"553","DOI":"10.1017\/S1471068418000091","article-title":"An iterative approach to precondition inference using constrained horn clauses","volume":"3","author":"Kafle","year":"2018","journal-title":"Theory Pract. Log. Program. 18,"},{"key":"S1471068419000152_ref14","first-page":"375","volume-title":"Proc. of PLDI 2009","author":"Gulwani","year":"2009"},{"key":"S1471068419000152_ref13","first-page":"12","volume-title":"Proc. SCOPES 2015","author":"Grech","year":"2015"},{"key":"S1471068419000152_ref12","first-page":"210","volume-title":"Proc. RTA 2004","volume":"3091","author":"Giesl","year":"2004"},{"key":"S1471068419000152_ref8","first-page":"255","volume-title":"Proc. SAS 1994","volume":"864","author":"Debray","year":"1994"},{"key":"S1471068419000152_ref4","first-page":"99","volume-title":"Proc. TACAS 2017","volume":"10205","author":"Borralleras","year":"2017"},{"key":"S1471068419000152_ref1","first-page":"221","volume-title":"Proc. of SAS 2008","volume":"5079","author":"Albert","year":"2008"},{"key":"S1471068419000152_ref9","unstructured":"Flores-Montoya, A. 2017. Cost analysis of programs based on the refinement of cost relations. Ph.D. thesis, Darmstadt University of Technology, Germany."},{"key":"S1471068419000152_ref2","first-page":"157","volume-title":"Proc. of ESOP\u201907","volume":"4421","author":"Albert","year":"2007"},{"key":"S1471068419000152_ref3","first-page":"1","article-title":"Parallel Cost Analysis","volume":"4","author":"Albert","year":"2018","journal-title":"ACM Trans. Comput. Log. 19,"},{"key":"S1471068419000152_ref18","unstructured":"Serrano, A. , L\u00f3pez-Garca, P. , Bueno, F. , and Hermenegildo, M. V. 2013. Sized type analysis for logic programs. Theory Pract. Log. Program. 13, 4-5-Online-Supplement."},{"key":"S1471068419000152_ref17","first-page":"348","volume-title":"Proc. ICLP 2007","volume":"4670","author":"Navas","year":"2007"},{"key":"S1471068419000152_ref22","doi-asserted-by":"crossref","first-page":"528","DOI":"10.1145\/361002.361016","article-title":"Mechanical Program Analysis","volume":"9","author":"Wegbreit","year":"1975","journal-title":"Communications ACM 18"},{"key":"S1471068419000152_ref11","first-page":"125","volume-title":"Proc. PPDP 2015","author":"Garcia","year":"2015"},{"key":"S1471068419000152_ref5","first-page":"13:1","article-title":"Analyzing runtime and size complexity of integer programs","volume":"4","author":"Brockschmidt","year":"2016","journal-title":"ACM Trans. Program. Lang. Syst. 38"},{"key":"S1471068419000152_ref6","first-page":"84","volume-title":"Proc. POPL 1978","author":"Cousot","year":"1978"},{"key":"S1471068419000152_ref16","first-page":"81","volume-title":"Proc. FOPARA 2015","volume":"9964","author":"Liqat","year":"2015"},{"key":"S1471068419000152_ref10","first-page":"275","volume-title":"Proc. APLAS 2014","volume":"8858","author":"Flores-Montoya","year":"2014"},{"key":"S1471068419000152_ref19","first-page":"703","volume-title":"Proc. of CAV 2011","author":"Sharma","year":"2011"},{"key":"S1471068419000152_ref7","doi-asserted-by":"crossref","first-page":"826","DOI":"10.1145\/161468.161472","article-title":"Cost analysis of logic programs","volume":"5","author":"Debray","year":"1993","journal-title":"ACM Trans. Program. Lang. Syst. 15,"}],"container-title":["Theory and Practice of Logic Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S1471068419000152","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,15]],"date-time":"2019-10-15T04:26:25Z","timestamp":1571113585000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1471068419000152\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,9]]},"references-count":22,"journal-issue":{"issue":"5-6","published-print":{"date-parts":[[2019,9]]}},"alternative-id":["S1471068419000152"],"URL":"https:\/\/doi.org\/10.1017\/s1471068419000152","relation":{},"ISSN":["1471-0684","1475-3081"],"issn-type":[{"value":"1471-0684","type":"print"},{"value":"1475-3081","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,9]]}}}