{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,13]],"date-time":"2025-05-13T22:00:49Z","timestamp":1747173649664,"version":"3.40.5"},"reference-count":38,"publisher":"Cambridge University Press (CUP)","issue":"3","license":[{"start":{"date-parts":[[2019,9,5]],"date-time":"2019-09-05T00:00:00Z","timestamp":1567641600000},"content-version":"unspecified","delay-in-days":0,"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":[[2020,5]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>In order to automatically infer the resource consumption of programs, analyzers track how <jats:italic>data sizes<\/jats:italic> change along program\u2019s execution. Typically, analyzers measure the sizes of data by applying <jats:italic>norms<\/jats:italic> which are mappings from data to natural numbers that represent the sizes of the corresponding data. When norms are defined by taking type information into account, they are named <jats:italic>typed-norms<\/jats:italic>. This article presents a transformational approach to resource analysis with typed-norms that are inferred by a data-flow analysis. The analysis is based on a transformation of the program into an <jats:italic>intermediate abstract program<\/jats:italic> in which each variable is abstracted with respect to all considered norms which are valid for its type. We also present the data-flow analysis to automatically infer the required, useful, typed-norms from programs. Our analysis is formalized on a simple rule-based representation to which programs written in different programming paradigms (e.g., functional, logic, and imperative) can be automatically translated. Experimental results on standard benchmarks used by other type-based analyzers show that our approach is both efficient and accurate in practice.<\/jats:p>","DOI":"10.1017\/s1471068419000401","type":"journal-article","created":{"date-parts":[[2019,9,5]],"date-time":"2019-09-05T09:10:15Z","timestamp":1567674615000},"page":"310-357","source":"Crossref","is-referenced-by-count":4,"title":["A Transformational Approach to Resource Analysis with Typed-norms Inference"],"prefix":"10.1017","volume":"20","author":[{"given":"ELVIRA","family":"ALBERT","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7176-1881","authenticated-orcid":false,"given":"SAMIR","family":"GENAIM","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"RA\u00daL","family":"GUTI\u00c9RREZ","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1664-018X","authenticated-orcid":false,"given":"ENRIQUE","family":"MARTIN-MARTIN","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2019,9,5]]},"reference":[{"key":"S1471068419000401_ref12","unstructured":"Bossi, A. , Cocco, N. , and Fabris, M. 1991. Proving termination of logic programs by exploiting term properties. In APSOFT 1991: Proceedings of the International Joint Conference on Theory and Practice of Software Development, Brighton, UK, April 8\u201312, 1991, Volume 2: Advances in Distributed Computing (ADC) and Colloquium on Combining Paradigms for Software Developmemnt (CCPSD), Abramsky, S. and Maibaum, T. S. E. , Eds. Lecture Notes in Computer Science, vol. 494. Springer, 153\u2013180."},{"key":"S1471068419000401_ref36","doi-asserted-by":"publisher","DOI":"10.2140\/pjm.1955.5.285"},{"key":"S1471068419000401_ref32","unstructured":"Puebla, G. and Hermenegildo, M. 1996. Optimized algorithms for the incremental analysis of logic programs. In International Static Analysis Symposium (SAS 1996), vol. 1145. Lecture Notes in Computer Science. Springer-Verlag, 270\u2013284."},{"key":"S1471068419000401_ref17","unstructured":"Flores-Montoya, A. and H\u00e4hnle, R. 2014. Resource analysis of complex programs with cost equations. In Programming Languages and Systems \u2013 12th Asian Symposium, APLAS 2014, Singapore, November 17\u201319, 2014, Proceedings. LNCS, vol. 8858. Springer, 275\u2013295."},{"key":"S1471068419000401_ref14","doi-asserted-by":"publisher","DOI":"10.1023\/A:1012996816178"},{"key":"S1471068419000401_ref4","unstructured":"Albert, E. , Arenas, P. , Genaim, S. , G\u00f3mez-Zamalloa, M. , and Puebla, G. 2011. Cost analysis of concurrent OO programs. In Programming Languages and Systems - 9th Asian Symposium, APLAS 2011, Kenting, Taiwan, December 5\u20137, 2011. Proceedings, Yang, H. , Ed. Lecture Notes in Computer Science, vol. 7078. Springer, 238\u2013254."},{"key":"S1471068419000401_ref37","unstructured":"Vasconcelos, P. and Hammond, K. 2003. Inferring cost equations for recursive, polymorphic and higher-order functional programs. In Proceedings of the International Workshop on Implementation of Functional Languages. Lecture Notes in Computer Science, vol. 3145. Springer-Verlag, 86\u2013101."},{"key":"S1471068419000401_ref19","doi-asserted-by":"publisher","DOI":"10.1145\/507669.507666"},{"key":"S1471068419000401_ref8","first-page":"142","article-title":"Cost analysis of object-oriented bytecode programs","volume":"413","author":"Albert","year":"2012","journal-title":"Theoretical Computer Science (Special Issue on Quantitative Aspects of Programming Languages)"},{"key":"S1471068419000401_ref38","doi-asserted-by":"publisher","DOI":"10.1145\/361002.361016"},{"key":"S1471068419000401_ref15","doi-asserted-by":"publisher","DOI":"10.1145\/115372.115320"},{"key":"S1471068419000401_ref25","doi-asserted-by":"publisher","DOI":"10.1145\/237721.240882"},{"key":"S1471068419000401_ref23","doi-asserted-by":"publisher","DOI":"10.1145\/604131.604148"},{"key":"S1471068419000401_ref16","unstructured":"Flores-Montoya, A. 2016. Upper and lower amortized cost bounds of programs expressed as cost relations. In FM 2016: Formal Methods \u2013 21st International Symposium, Limassol, Cyprus, November 9\u201311, 2016, Proceedings, Fitzgerald, J. S. , Heitmeyer, C. L. , Gnesi, S. , and Philippou, A. , Eds. Lecture Notes in Computer Science, vol. 9995. Springer, 254\u2013273."},{"key":"S1471068419000401_ref21","unstructured":"Hoffmann, J. , Aehlig, K. , and Hofmann, M. 2012. Resource aware ML. In 24rd International Conference on Computer Aided Verification (CAV 2012). Lecture Notes in Computer Science, vol. 7358. Springer, 781\u2013786."},{"key":"S1471068419000401_ref24","unstructured":"Hughes, J. and Pareto, L. 1999. Recursion and dynamic data-structures in bounded space: Towards embedded ML programming. In Proc. of ICFP 1999. ACM Press, 70\u201381."},{"key":"S1471068419000401_ref33","unstructured":"Sands, D. 1990. Calculi for time analysis of functional programs. Ph.D. thesis, Department of Computing, Imperial College London."},{"key":"S1471068419000401_ref29","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-03811-6"},{"key":"S1471068419000401_ref9","unstructured":"Albert, E. , Genaim, S. , and Guti\u00e9rrez, R. 2014. A transformational approach to resource analysis with typed-norms. In Proc. of the 23rd International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR\u201913). Lecture Notes in Computer Science, vol. 8901. Springer, 38\u201353."},{"key":"S1471068419000401_ref11","unstructured":"Alonso-Blas, D. E. , Arenas, P. , and Genaim, S. 2011. Handling non-linear operations in the value analysis of COSTA. In Proceedings of the Bytecode 2011 Workshop, the Sixth Workshop on Bytecode Semantics, Verification, Analysis and Transformation (Bytecode). Electronic Notes in Theoretical Computer Science 279, 1. Elsevier, 3\u201317."},{"key":"S1471068419000401_ref6","unstructured":"Albert, E. , Arenas, P. , Genaim, S. , Puebla, G. , and Zanardini, D. 2007. Cost Analysis of Java Bytecode. In Programming Languages and Systems, 16th European Symposium on Programming, ESOP 2007, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2007, Braga, Portugal, March 24 \u2013 April 1, 2007, Proceedings, Nicola, R. D. , Ed. Lecture Notes in Computer Science, vol. 4421. Springer-Verlag, 157\u2013172."},{"key":"S1471068419000401_ref30","unstructured":"Vasconcelos, Pedro . 2008. Space cost analysis using sized types. Ph.D. thesis, School of Computer Science, University of St. Andrews."},{"key":"S1471068419000401_ref22","unstructured":"Hoffmann, J. , Das, A. , and Weng, S.-C. 2017. Towards automatic resource bound analysis for OCaml. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages. POPL 2017. ACM, New York, NY, USA, 359\u2013373."},{"key":"S1471068419000401_ref20","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068411000457"},{"key":"S1471068419000401_ref5","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-010-9174-1"},{"key":"S1471068419000401_ref13","doi-asserted-by":"publisher","DOI":"10.1145\/1216374.1216378"},{"key":"S1471068419000401_ref26","unstructured":"Johnsen, E. B. , H\u00e4hnle, R. , Sch\u00e4fer, J. , Schlatte, R. , and Steffen, M. 2012. ABS: A Core Language for abstract behavioral specification. In Formal Methods for Components and Objects - 9th International Symposium, FMCO 2010, Graz, Austria, November 29 - December 1, 2010. Revised Papers, Aichernig, B. K. , de Boer, F. S. , and Bonsangue, M. M. , Eds. Lecture Notes in Computer Science, vol. 6957. Springer, 142\u2013164."},{"key":"S1471068419000401_ref2","doi-asserted-by":"publisher","DOI":"10.1002\/stvr.1569"},{"key":"S1471068419000401_ref1","unstructured":"Agha, G. and Callsen, C. J. 1993. Actorspace: An open distributed programming paradigm. In Proceedings 4th ACM Conference on Principles and Practice of Parallel Programming, ACM SIGPLAN Notices, 23\u201332."},{"key":"S1471068419000401_ref27","unstructured":"King, A. , Shen, K. , and Benoy, F. 1997. Lower-bound time-complexity analysis of logic programs. In 1997 International Logic Programming Symposium, Maluszy\u0144ski, J. , Ed. MIT Press, Cambridge, MA, 261\u2013275."},{"key":"S1471068419000401_ref10","doi-asserted-by":"publisher","DOI":"10.1145\/2499937.2499943"},{"key":"S1471068419000401_ref3","unstructured":"Albert, E. , Arenas, P. , Flores-Montoya, A. , Genaim, S. , G\u00f3mez-Zamalloa, M. , Martin-Martin, E. , Puebla, G. , and Rom\u00e1n-D\u00edez, G. 2014. SACO: Static analyzer for concurrent objects. In Tools and Algorithms for the Construction and Analysis of Systems \u2013 20th International Conference, TACAS 2014, \u00c1brah\u00e1m, E. and Havelund, K. , Eds. Lecture Notes in Computer Science, vol. 8413. Springer, 562\u2013567."},{"key":"S1471068419000401_ref28","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(92)90035-2"},{"key":"S1471068419000401_ref7","unstructured":"Albert, E. , Arenas, P. , Genaim, S. , Puebla, G. , and Zanardini, D. 2008. Removing useless variables in cost analysis of Java Bytecode. In Proceedings of the 2008 ACM Symposium on Applied Computing (SAC), Fortaleza, Ceara, Brazil, March 16\u201320, 2008, Wainwright, R. L. and Haddad, H. , Eds. ACM, 368\u2013375."},{"key":"S1471068419000401_ref35","first-page":"739","article-title":"Resource usage analysis of logic programs via abstract interpretation using sized types","volume":"14","author":"Serrano","year":"2014","journal-title":"TPLP"},{"volume-title":"Types and Programming Languages","year":"2002","author":"Pierce","key":"S1471068419000401_ref31"},{"key":"S1471068419000401_ref18","unstructured":"Genaim, S. , Codish, M. , Gallagher, J. , and Lagoon, V. 2002. Combining norms to prove termination. In 3rd International Workshop on Verification, Model Checking, and Abstract Interpretation (VMCAI\u201902), Goos, G. , Hartmanis, J. , and van Leeuwen, J. , Eds. Lecture Notes in Computer Science, vol. 2294. Springer, 123\u2013138."},{"key":"S1471068419000401_ref34","unstructured":"Serrano, A. , L\u00f3pez-Garc\u00eda, P. , Bueno, F. , and Hermenegildo, M. V. 2013. Sized type analysis for logic programs. Theory and Practice of Logic Programming 13, 4-5-Online-Supplement (August)."}],"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\/S1471068419000401","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,5]],"date-time":"2020-11-05T09:10:09Z","timestamp":1604567409000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1471068419000401\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,9,5]]},"references-count":38,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2020,5]]}},"alternative-id":["S1471068419000401"],"URL":"https:\/\/doi.org\/10.1017\/s1471068419000401","relation":{},"ISSN":["1471-0684","1475-3081"],"issn-type":[{"type":"print","value":"1471-0684"},{"type":"electronic","value":"1475-3081"}],"subject":[],"published":{"date-parts":[[2019,9,5]]}}}