{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T20:14:30Z","timestamp":1784837670628,"version":"3.55.0"},"reference-count":28,"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>Control-flow refinement refers to program transformations whose purpose is to make implicit control-flow explicit, and is used in the context of program analysis to increase precision. Several techniques have been suggested for different programming models, typically tailored to improving precision for a particular analysis. In this paper we explore the use of partial evaluation of Horn clauses as a general-purpose technique for control-flow refinement for integer transitions systems. These are control-flow graphs where edges are annotated with linear constraints describing transitions between corresponding nodes, and they are used in many program analysis tools. Using partial evaluation for control-flow refinement has the clear advantage over other approaches in that soundness follows from the general properties of partial evaluation; in particular, properties such as termination and complexity are preserved. We use a partial evaluation algorithm incorporating property-based abstraction, and show how the right choice of properties allows us to prove termination and to infer complexity of challenging programs that cannot be handled by state-of-the-art tools. We report on the integration of the technique in a termination analyzer, and its use as a preprocessing step for several cost analyzers.<\/jats:p>","DOI":"10.1017\/s1471068419000310","type":"journal-article","created":{"date-parts":[[2019,9,20]],"date-time":"2019-09-20T09:06:21Z","timestamp":1568970381000},"page":"990-1005","source":"Crossref","is-referenced-by-count":19,"title":["Control-Flow Refinement by Partial Evaluation, and its Application to Termination and Cost Analysis"],"prefix":"10.1017","volume":"19","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4443-7824","authenticated-orcid":false,"given":"JES\u00daS J.","family":"DOM\u00c9NECH","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6984-7419","authenticated-orcid":false,"given":"JOHN P.","family":"GALLAGHER","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7176-1881","authenticated-orcid":false,"given":"SAMIR","family":"GENAIM","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2019,9,20]]},"reference":[{"key":"S1471068419000310_ref11","first-page":"51","volume-title":"LOPSTR 2012","volume":"7844","author":"De Angelis","year":"2012"},{"key":"S1471068419000310_ref14","volume-title":"Cost analysis of programs based on the refinement of cost relations","author":"Flores-Montoya","year":"2017"},{"key":"S1471068419000310_ref22","unstructured":"Leuschel, M. and Massart, T. 2000. Infinite state model checking by abstract interpretation and program specialisation. In LOPSTR\u201999, A. Bossi , Ed. LNCS, vol. 1817. 63\u201382."},{"key":"S1471068419000310_ref3","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2007.08.001"},{"key":"S1471068419000310_ref10","first-page":"84","volume-title":"Fifth Annual ACM Symposium on Principles of Programming Languages, POPL\u201978","author":"Cousot","year":"1978"},{"key":"S1471068419000310_ref24","first-page":"107","volume-title":"SAS 2006","volume":"4134","author":"Puebla","year":"2006"},{"key":"S1471068419000310_ref18","unstructured":"iRank 2019. iRankFinder. http:\/\/irankfinder.loopkiller.com."},{"key":"S1471068419000310_ref12","unstructured":"Dom\u00e9nech, J. J. , Gallagher, J. P. , and Genaim, S. 2019. Control-flow refinement by partial evaluation, and its application to termination and cost analysis. CoRR abs\/1907.12345. https:\/\/arxiv.org\/abs\/1907.12345."},{"key":"S1471068419000310_ref7","first-page":"99","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems, TACAS\u201917","volume":"10205","author":"Borralleras","year":"2017"},{"key":"S1471068419000310_ref17","unstructured":"Gulwani, S. , Jain, S. , and Koskinen, E. 2009. Control-flow refinement and progress invariants for bound analysis. In Programming Language Design and Implementation, PLDI\u201909, M. Hind and A. Diwan , Eds. ACM, 375\u2013385."},{"key":"S1471068419000310_ref15","unstructured":"Flores-Montoya, A. and H\u00e4hnle, R. 2014. Resource analysis of complex programs with cost equations. In Asian Symposium on Programming Languages and Systems, APLAS 2014, J. Garrigue , Ed. LNCS, vol. 8858. Springer, 275\u2013295."},{"key":"S1471068419000310_ref26","doi-asserted-by":"crossref","first-page":"703","DOI":"10.1007\/978-3-642-22110-1_57","volume-title":"Computer Aided Verification, CAV 2011","volume":"6806","author":"Sharma","year":"2011"},{"key":"S1471068419000310_ref20","doi-asserted-by":"publisher","DOI":"10.1145\/982158.982159"},{"key":"S1471068419000310_ref27","unstructured":"TERMCOMP 2019. http:\/\/termination-portal.org\/wiki\/Termination_Competition_2019."},{"key":"S1471068419000310_ref1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-010-9174-1"},{"key":"S1471068419000310_ref19","first-page":"553","article-title":"An iterative approach to precondition inference using constrained Horn clauses","volume":"3","author":"Kafle","year":"2018","journal-title":"TPLP 18"},{"key":"S1471068419000310_ref2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15769-1_8"},{"key":"S1471068419000310_ref4","unstructured":"Bagnara, R. , Mesnard, F. , Pescetti, A. , and Zaffanella, E. 2012. A new look at the automatic synthesis of linear ranking functions. Inf. Comput. 215, 47\u201367."},{"key":"S1471068419000310_ref5","doi-asserted-by":"publisher","DOI":"10.1145\/2629488"},{"key":"S1471068419000310_ref6","doi-asserted-by":"crossref","first-page":"601","DOI":"10.1007\/978-3-319-63390-9_32","volume-title":"Computer Aided Verification, CAV 2017","volume":"10427","author":"Ben-Amram","year":"2017"},{"key":"S1471068419000310_ref8","first-page":"387","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems TACAS 2016","volume":"9636","author":"Brockschmidt","year":"2016"},{"key":"S1471068419000310_ref9","doi-asserted-by":"publisher","DOI":"10.1145\/2866575"},{"key":"S1471068419000310_ref13","doi-asserted-by":"crossref","first-page":"281","DOI":"10.3233\/FI-2012-738","article-title":"Improving reachability analysis of infinite state systems by specialization","volume":"3","author":"Fioravanti","year":"2012","journal-title":"Fundam. Inform. 119"},{"key":"S1471068419000310_ref16","unstructured":"Gallagher, J. P. 2019. Polyvariant program specialisation with property-based abstraction. In Pre-proceedings of Verification and Program Transformation, VPT\u201919, A. Lisitsa and A. P. Nemytykh , Eds. Available at http:\/\/refal.botik.ru\/vpt\/vpt2019\/VPT2019_paper_5.pdf. Accepted for EPTCS."},{"key":"S1471068419000310_ref21","unstructured":"Leuschel, M. , Elphick, D. , Varea, M. , Craig, S. , and Fontaine, M. 2006. The Ecce and Logen partial evaluators and their web interfaces. In PEPM 2006, J. Hatcliff and F. Tip , Eds. ACM, 88\u201394."},{"key":"S1471068419000310_ref23","doi-asserted-by":"crossref","first-page":"239","DOI":"10.1007\/978-3-540-24622-0_20","volume-title":"Verification, Model Checking, and Abstract Interpretation, VMCAI\u201904","volume":"2937","author":"Podelski","year":"2004"},{"key":"S1471068419000310_ref25","first-page":"75","volume-title":"Technical report BRICS-NS-99-1","author":"Puebla","year":"1999"},{"key":"S1471068419000310_ref28","unstructured":"TPDB 2019. http:\/\/termination-portal.org\/wiki\/TPDB."}],"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\/S1471068419000310","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,12,7]],"date-time":"2019-12-07T12:21:49Z","timestamp":1575721309000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1471068419000310\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,9]]},"references-count":28,"journal-issue":{"issue":"5-6","published-print":{"date-parts":[[2019,9]]}},"alternative-id":["S1471068419000310"],"URL":"https:\/\/doi.org\/10.1017\/s1471068419000310","relation":{},"ISSN":["1471-0684","1475-3081"],"issn-type":[{"value":"1471-0684","type":"print"},{"value":"1475-3081","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,9]]}}}