{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,4]],"date-time":"2023-09-04T21:11:55Z","timestamp":1693861915414},"reference-count":27,"publisher":"Cambridge University Press (CUP)","license":[{"start":{"date-parts":[[2015,10,29]],"date-time":"2015-10-29T00:00:00Z","timestamp":1446076800000},"content-version":"unspecified","delay-in-days":301,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2015]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Proving bounds on the resource consumption of a program by statically analyzing its source code is an important and well-studied problem. Automatic approaches for numeric programs with side effects usually apply abstract interpretation-based invariant generation to derive bounds on loops and recursion depths of function calls. This article presents an alternative approach to resource-bound analysis for numeric and heap-manipulating programs that uses type-based amortized resource analysis. As a first step towards the analysis of imperative code, the technique is developed for a first-order ML-like language with unsigned integers and arrays. The analysis automatically derives bounds that are multivariate polynomials in the numbers and the lengths of the arrays in the input. Experiments with example programs demonstrate two main advantages of amortized analysis over current abstract interpretation\u2013based techniques. For one thing, amortized analysis can handle programs with non-linear intermediate values like<jats:italic>f<\/jats:italic>((<jats:italic>n + m<\/jats:italic>)<jats:sup>2<\/jats:sup>). For another thing, amortized analysis is compositional and works naturally for compound programs like<jats:italic>f<\/jats:italic>(<jats:italic>g<\/jats:italic>(<jats:italic>x<\/jats:italic>)).<\/jats:p>","DOI":"10.1017\/s0956796815000192","type":"journal-article","created":{"date-parts":[[2015,10,29]],"date-time":"2015-10-29T04:59:28Z","timestamp":1446094768000},"source":"Crossref","is-referenced-by-count":8,"title":["Type-based amortized resource analysis with integers and arrays"],"prefix":"10.1017","volume":"25","author":[{"given":"JAN","family":"HOFFMANN","sequence":"first","affiliation":[]},{"given":"ZHONG","family":"SHAO","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2015,10,29]]},"reference":[{"key":"S0956796815000192_ref25","doi-asserted-by":"crossref","unstructured":"Sinn M. , Zuleger F. & Veith H. (2014) A simple and scalable static analysis for bound analysis and amortized complexity analysis. In Proceedings of 26th International Conference on Computer Aided Verification. (CAV'14), Vienna, Austria, pp. 743\u2013759.","DOI":"10.1007\/978-3-319-08867-9_50"},{"key":"S0956796815000192_ref19","doi-asserted-by":"crossref","unstructured":"Hoffmann J. , Aehlig K. & Hofmann M. (2012b) Resource aware ML. In Proceedings of 24th International Conference on Computer Aided Verification. (CAV'12), Berkeley, CA, USA, pp. 781\u2013786.","DOI":"10.1007\/978-3-642-31424-7_64"},{"key":"S0956796815000192_ref18","doi-asserted-by":"publisher","DOI":"10.1145\/2362389.2362393"},{"key":"S0956796815000192_ref17","doi-asserted-by":"crossref","unstructured":"Hoffmann J. , Aehlig K. & Hofmann M. (2011) Multivariate amortized resource analysis. In Proceedings of 38th ACM Symposium on Principles of Programming Languages. (POPL'11), Austin, TX, USA, pp. 357\u2013370.","DOI":"10.1145\/1926385.1926427"},{"key":"S0956796815000192_ref24","doi-asserted-by":"publisher","DOI":"10.1007\/11823230_2"},{"key":"S0956796815000192_ref26","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-5662-3"},{"key":"S0956796815000192_ref14","doi-asserted-by":"crossref","unstructured":"Hoffmann J. & Hofmann M. (2010a) Amortized resource analysis with polynomial potential. In Proceedings of the 19th European Symposium on Programming. (ESOP'10), Paphos, Cyprus, pp. 287\u2013306.","DOI":"10.1007\/978-3-642-11957-6_16"},{"key":"S0956796815000192_ref20","doi-asserted-by":"crossref","unstructured":"Hofmann M. & Jost S. (2003) Static prediction of heap space usage for first-order functional programs. In Proceedings of 30th ACM Symposium on Principles of Programming Languages. (POPL'03), New Orleans, Louisisana, pp. 185\u2013197.","DOI":"10.1145\/604131.604148"},{"key":"S0956796815000192_ref11","unstructured":"Cousot P. & Halbwachs N. (1978) Automatic discovery of linear restraints among variables of a program. In Proceedings of the 5th ACM Symposium on Principles Programming Languages. (POPL'78), Tucson, Arizona, USA, pp. 84\u201396."},{"key":"S0956796815000192_ref27","doi-asserted-by":"crossref","unstructured":"Zuleger F. , Sinn M. , Gulwani S. & Veith H. (2011) Bound analysis of imperative programs with the size-change abstraction. In Proceedings of 18th International Static Analysis Symposium. (SAS'11), Venice, Italy, pp. 280\u2013297.","DOI":"10.1007\/978-3-642-23702-7_22"},{"key":"S0956796815000192_ref13","doi-asserted-by":"publisher","DOI":"10.1145\/1594834.1480898"},{"key":"S0956796815000192_ref1","unstructured":"Aehlig K. , Hofmann M. & Hoffmann J. (2010\u20132013) RAML Web Site. Available at: http:\/\/raml.tcs.ifi.lmu.de."},{"key":"S0956796815000192_ref2","doi-asserted-by":"crossref","unstructured":"Albert E. , Arenas P. , Genaim S. , G\u00f3mez-Zamalloa M. & Puebla G. (2012a) Automatic inference of resource consumption bounds. In Logic for Programming, Artificial Intelligence, and Reasoning, 18th Conference (LPAR'18), M\u00e9rida, Venezuela, pp. 1\u201311.*","DOI":"10.1007\/978-3-642-28717-6_1"},{"key":"S0956796815000192_ref3","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-010-9174-1"},{"key":"S0956796815000192_ref4","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2011.07.009"},{"key":"S0956796815000192_ref15","doi-asserted-by":"crossref","unstructured":"Hoffmann J. & Hofmann M. (2010b) Amortized resource analysis with polymorphic recursion and partial big-step operational semantics. In Proceedings of the 8th Asian Symposium on Programming Languages and Systems. (APLAS'10). Shanghai, China, pp. 172\u2013187.","DOI":"10.1007\/978-3-642-17164-2_13"},{"key":"S0956796815000192_ref5","doi-asserted-by":"crossref","unstructured":"Alias C. , Darte A. , Feautrier P. & Gonnord L. (2010) Multi-dimensional rankings, program termination, and complexity bounds of flowchart programs. In Proceedings of 17th International Static Analysis Symposium (SAS'10), Perpignan, France, pp. 117\u2013133.","DOI":"10.1007\/978-3-642-15769-1_8"},{"key":"S0956796815000192_ref6","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2011.11.002"},{"key":"S0956796815000192_ref7","doi-asserted-by":"crossref","unstructured":"Alonso-Blas D. E. & Genaim S. (2012) On the limits of the classical approach to cost analysis. In Proceedings of 19th International Static Analysis Symposium (SAS'12), Deauville, France, pp. 405\u2013421.","DOI":"10.1007\/978-3-642-33125-1_27"},{"key":"S0956796815000192_ref8","doi-asserted-by":"crossref","unstructured":"Brockschmidt M. , Emmes F. , Falke S. , Fuhs C. & Giesl J. (2014) Alternating runtime and size complexity analysis of integer programs. In Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. (TACAS'14), Held as Part of the European Joint Conferences on Theory and Practice of Software, (ETAPS'14), Grenoble, France, pp. 140\u2013155.","DOI":"10.1007\/978-3-642-54862-8_10"},{"key":"S0956796815000192_ref9","doi-asserted-by":"crossref","unstructured":"Carbonneaux Q. , Hoffmann J. , Ramananandro T. & Shao Z. (2014) End-to-end verification of stack-space bounds for C programs. In Proceedings of the Conference on Programming Language Design and Implementation. (PLDI'14), Edinburgh, Scotland, p. 30.","DOI":"10.1145\/2666356.2594301"},{"key":"S0956796815000192_ref10","doi-asserted-by":"crossref","unstructured":"Carbonneaux Q. , Hoffmann J. & Shao Z. (2015) Compositional certified resource bounds. In Proceedings of 36th Conference on Programming Language Design and Implementation (PLDI'15). Portland, OR, USA, pp. 467\u2013478. Forthcoming.","DOI":"10.1145\/2737924.2737955"},{"key":"S0956796815000192_ref12","unstructured":"Gulavani B. S. & Gulwani S. (2008) A numerical abstract domain based on expression abstraction and max operator with application in timing analysis. In Proceedings of the 20th International Conference Computer Aided Verification. (CAV '08), Princeton, NJ, USA, pp. 370\u2013384."},{"key":"S0956796815000192_ref16","doi-asserted-by":"crossref","unstructured":"Hoffmann J. & Shao Z. (2014) Type-based amortized resource analysis with integers and arrays. In Proceedings of 12th International Symposium on Functional and Logic Programming. (FLOPS'14), Kanazawa, Japan, pp. 152\u2013168.","DOI":"10.1007\/978-3-319-07151-0_10"},{"key":"S0956796815000192_ref21","doi-asserted-by":"crossref","unstructured":"Leroy X. (2006) Coinductive big-step operational semantics. In Proceedings of 15th European Symposium on Programming. (ESOP'06), Vienna, Austria, pp. 54\u201368.","DOI":"10.1007\/11693024_5"},{"key":"S0956796815000192_ref22","unstructured":"Min\u00e9 A. (2004) Weakly Relational Numerical Abstract Domains. Ph.D. thesis, \u00c9cole Polytechnique, Paris, France."},{"key":"S0956796815000192_ref23","doi-asserted-by":"publisher","DOI":"10.1016\/0097-3165(72)90084-2"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796815000192","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,8,15]],"date-time":"2023-08-15T17:30:25Z","timestamp":1692120625000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796815000192\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"references-count":27,"alternative-id":["S0956796815000192"],"URL":"https:\/\/doi.org\/10.1017\/s0956796815000192","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]},"article-number":"e17"}}