{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,1]],"date-time":"2026-10-01T14:35:17Z","timestamp":1790865317997,"version":"4.1.0"},"reference-count":54,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2010,4,29]],"date-time":"2010-04-29T00:00:00Z","timestamp":1272499200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2011,2]]},"DOI":"10.1007\/s10817-010-9174-1","type":"journal-article","created":{"date-parts":[[2010,4,28]],"date-time":"2010-04-28T06:13:30Z","timestamp":1272435210000},"page":"161-203","source":"Crossref","is-referenced-by-count":120,"title":["Closed-Form Upper Bounds in Static Cost Analysis"],"prefix":"10.1007","volume":"46","author":[{"given":"Elvira","family":"Albert","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Puri","family":"Arenas","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Samir","family":"Genaim","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Germ\u00e1n","family":"Puebla","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2010,4,29]]},"reference":[{"key":"9174_CR1","unstructured":"Aho, A.V., Hopcroft, J.E., Ullman, J.D.: The Design and Analysis of Computer Algorithms. Addison-Wesley, Reading (1974)"},{"key":"9174_CR2","doi-asserted-by":"crossref","unstructured":"Albert, E., Arenas, P., Codish, M., Genaim, S., Puebla, G., Zanardini, D.: Termination analysis of Java bytecode. In: 10th IFIP International Conference on Formal Methods for Open Object-based Distributed Systems (FMOODS\u201908). Lecture Notes in Computer Science, vol.\u00a05051, pp.\u00a02\u201318. Springer, Heidelberg (2008)","DOI":"10.1007\/978-3-540-68863-1_2"},{"key":"9174_CR3","volume-title":"1st International Workshop on Foundational and Practical Aspects of Resource Analysis (FOPARA\u201909). Lecture Notes in Computer Science","author":"E Albert","year":"2009","unstructured":"Albert, E., Arenas, P., Genaim, S., Herraiz, I., Puebla, G.: Comparing cost functions in resource analysis. In: 1st International Workshop on Foundational and Practical Aspects of Resource Analysis (FOPARA\u201909). Lecture Notes in Computer Science. Springer, Heidelberg (2009)"},{"key":"9174_CR4","doi-asserted-by":"crossref","unstructured":"Albert, E., Arenas, P., Genaim, S., Puebla, G.: Automatic inference of upper bounds for recurrence relations in cost analysis. In: 15th International Symposium on Static Analysis (SAS\u201908). Lecture Notes in Computer Science, vol. 5079, pp.\u00a0221\u2013237 (2008)","DOI":"10.1007\/978-3-540-69166-2_15"},{"key":"9174_CR5","unstructured":"Albert, E., Arenas, P., Genaim, S., Puebla, G.: Cost relation systems: a language\u2013independent target language for cost analysis. In: 8th Spanish Conference on Programming and Computer Languages (PROLE\u201908), vol. 17615 of Electronic Notes in Theoretical Computer Science. Elsevier (2008)"},{"key":"9174_CR6","doi-asserted-by":"crossref","unstructured":"Albert, E., Arenas, P., Genaim, S., Puebla, G., Zanardini, D.: Cost analysis of Java bytecode. In: 16th European Symposium on Programming, (ESOP\u201907). Lecture Notes in Computer Science, vol.\u00a04421, pp.\u00a0157\u2013172. Springer (2007)","DOI":"10.1007\/978-3-540-71316-6_12"},{"key":"9174_CR7","doi-asserted-by":"crossref","unstructured":"Albert, E., Arenas, P., Genaim, S., Puebla, G., Zanardini, D.: COSTA: design and implementation of a cost and termination analyzer for Java bytecode. In: 6th International Symposioum on Formal Methods for Components and Objects (FMCO\u201908). Lecture Notes in Computer Science, no.\u00a05382, pp.\u00a0113\u2013133. Springer (2007)","DOI":"10.1007\/978-3-540-92188-2_5"},{"key":"9174_CR8","doi-asserted-by":"crossref","unstructured":"Albert, E., Arenas, P., Genaim, S., Puebla, G., Zanardini, D.: Experiments in cost analysis of Java bytecode. In 2nd Workshop on Bytecode Semantics, Verification, Analysis and Transformation (BYTECODE\u201907), vol. 190, Issue 1 of Electronic Notes in Theoretical Computer Science. Elsevier (2007)","DOI":"10.1016\/j.entcs.2007.02.061"},{"key":"9174_CR9","doi-asserted-by":"crossref","unstructured":"Albert, E., Arenas, P., Genaim, S., Puebla, G., Zanardini, D.: Resource usage analysis and its application to resource certification. In: 9th International School on Foundations of Security Analysis and Design (FOSAD\u201909). Lecture Notes in Computer Science, no.\u00a05705, pp.\u00a0258\u2013288. Springer (2009)","DOI":"10.1007\/978-3-642-03829-7_9"},{"key":"9174_CR10","doi-asserted-by":"crossref","unstructured":"Albert, E., Genaim, S., G\u00f3mez-Zamalloa, M.: Heap space analysis of Java bytecode. In: 6th International Symposium on Memory Management (ISMM\u201907), pp.\u00a0105\u2013116. ACM Press (2007)","DOI":"10.1145\/1296907.1296922"},{"key":"9174_CR11","doi-asserted-by":"crossref","unstructured":"Albert, E., Genaim, S., G\u00f3mez-Zamalloa, M.: Live Heap space analysis for languages with garbage collection. In: 8th International Symposium on Memory management (ISMM\u201909). ACM Press (2009)","DOI":"10.1145\/1542431.1542450"},{"key":"9174_CR12","doi-asserted-by":"crossref","unstructured":"Aspinall, D., Gilmore, S., Hofmann, M., Sannella, D., Stark, I.: Mobile resource guarantees for smart devices. In: Workshop on Construction and Analysis of Safe, Secure and Interoperable Smart Devices (CASSIS\u201904). Lecture Notes in Computer Science, vol.\u00a03362, pp.\u00a01\u201327. Springer (2005)","DOI":"10.1007\/978-3-540-30569-9_1"},{"issue":"1\u20132","key":"9174_CR13","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/j.scico.2007.08.001","volume":"72","author":"R Bagnara","year":"2008","unstructured":"Bagnara, R., Hill, P.M., Zaffanella, E.: The Parma Polyhedra Library: toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Sci. Comput. Program. 72(1\u20132), 3\u201321 (2008)","journal-title":"Sci. Comput. Program."},{"key":"9174_CR14","unstructured":"Bagnara, R., Pescetti, A., Zaccagnini, A., Zaffanella, E.: PURRS: towards computer algebra support for fully automatic worst-case complexity analysis. Technical report (2005). http:\/\/arXiv.org.\/abs\/cs\/0512056"},{"key":"9174_CR15","unstructured":"Batchelder, P.M.: An introduction to linear difference equations. Dover Publications (1967)"},{"issue":"3","key":"9174_CR16","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1145\/1353445.1353450","volume":"30","author":"AM Ben-Amram","year":"2008","unstructured":"Ben-Amram, A.M.: Size-change termination with difference constraints. ACM Trans. Program. Lang. Syst. 30(3), 31 (2008) (Article 16)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"9174_CR17","doi-asserted-by":"crossref","unstructured":"Ben-Amram, A.M., Jones, N.D., Kristiansen L.: Linear, polynomial or exponential? Complexity inference in polynomial time. In: Logic and Theory of Algorithms, 4th Conference on Computability in Europe, (CiE\u201908). Lecture Notes in Computer Science, vol.\u00a05028, pp.\u00a067\u201376. Springer (2008)","DOI":"10.1007\/978-3-540-69407-6_7"},{"issue":"1\u20132","key":"9174_CR18","doi-asserted-by":"crossref","first-page":"79","DOI":"10.1016\/j.tcs.2003.10.022","volume":"318","author":"R Benzinger","year":"2004","unstructured":"Benzinger, R.: Automated higher-order complexity analysis. Theor. Comp. Sci. 318(1\u20132), 79\u2013103 (2004)","journal-title":"Theor. Comp. Sci."},{"key":"9174_CR19","doi-asserted-by":"crossref","unstructured":"Bonfante, G., Marion, J.-Y., Moyen, J.-Y.: Quasi-interpretations and small space bounds. In: 16th International Conference on Rewriting Techniques and Applications (RTA\u201905). Lecture Notes in Computer Science, vol.\u00a03467, pp.\u00a0150\u2013164 (2005)","DOI":"10.1007\/978-3-540-32033-3_12"},{"key":"9174_CR20","doi-asserted-by":"crossref","unstructured":"Braverman, M.: Termination of integer linear programs. In: 18th Computer Aided Verification (CAV\u201906). Lecture Notes in Computer Science, vol.\u00a04144, pp.\u00a0372\u2013385. Springer (2006)","DOI":"10.1007\/11817963_34"},{"key":"9174_CR21","doi-asserted-by":"crossref","unstructured":"Chander, A., Espinosa, D., Islam, N., Lee, P., Necula, G.: Enforcing resource bounds via static verification of dynamic checks. In: 14th European Symposium on Programming (ESOP\u201905). Lecture Notes in Computer Science, vol.\u00a03444, pp.\u00a0311\u2013325. Springer (2005)","DOI":"10.1007\/978-3-540-31987-0_22"},{"key":"9174_CR22","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: ACM Symposium on Principles of Programming Languages (POPL\u201977), pp.\u00a0238\u2013252. ACM Press (1977)","DOI":"10.1145\/512950.512973"},{"key":"9174_CR23","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: ACM Symposium on Principles of Programming Languages (POPL\u201978), pp.\u00a084\u201397. ACM Press (1978)","DOI":"10.1145\/512760.512770"},{"key":"9174_CR24","doi-asserted-by":"crossref","unstructured":"Craig, S.-J., Leuschel, M.: Self-tuning resource aware specialisation for prolog. In: 7th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming (PPDP\u201905), pp.\u00a023\u201334. ACM Press (2005)","DOI":"10.1145\/1069774.1069777"},{"key":"9174_CR25","doi-asserted-by":"crossref","unstructured":"Crary, K., Weirich, S.: Resource bound certification. In: 27th ACM Symposium on Principles of Programming Languages (POPL\u201905), pp.\u00a0184\u2013198. ACM Press (2000)","DOI":"10.1145\/325694.325716"},{"issue":"5","key":"9174_CR26","doi-asserted-by":"crossref","first-page":"826","DOI":"10.1145\/161468.161472","volume":"15","author":"SK Debray","year":"1993","unstructured":"Debray, S.K., Lin, N.W.: Cost Analysis of Logic Programs. ACM Trans. Program. Lang. Syst. 15(5), 826\u2013875 (1993)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"9174_CR27","doi-asserted-by":"crossref","unstructured":"Floyd, R.W.: Assigning meanings to programs. In: Proceedings of Symposium in Applied Mathematics, vol. 19, Mathematical Aspects of Computer Science, pp.\u00a019\u201332. American Mathematical Society, Providence, RI (1967)","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"9174_CR28","doi-asserted-by":"crossref","unstructured":"G\u00f3mez, G., Liu, Y.A.: Automatic time-bound analysis for a higher-order language. In: Proceedings of the ACM SIGPLAN 2002 Workshop on Partial Evaluation and Semantics-Based Program Manipulation, pp.\u00a075\u201388. ACM Press (2002)","DOI":"10.1145\/503032.503039"},{"issue":"1\u20132","key":"9174_CR29","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1016\/j.scico.2005.02.006","volume":"58","author":"M Hermenegildo","year":"2005","unstructured":"Hermenegildo, M., Puebla, G., Bueno, F., L\u00f3pez-Garc\u00eda, P.: Integrated program debugging, verification, and optimization using abstract interpretation (and The Ciao System Preprocessor). Sci. Comput. Program. 58(1\u20132), 115\u2013140 (2005)","journal-title":"Sci. Comput. Program."},{"issue":"1","key":"9174_CR30","doi-asserted-by":"crossref","first-page":"185","DOI":"10.1145\/42267.42275","volume":"35","author":"T Hickey","year":"1988","unstructured":"Hickey, T., Cohen, J.: Automating program analysis. J. ACM 35(1), 185\u2013220 (1988)","journal-title":"J. ACM"},{"key":"9174_CR31","doi-asserted-by":"crossref","unstructured":"Hofmann, M., Jost, S.: Static prediction of heap space usage for first-order functional programs. In: 30th Symposium on Principles of Programming Languages (POPL\u201903), pp.\u00a0185\u2013197. ACM Press, New York (2003)","DOI":"10.1145\/604131.604148"},{"issue":"20","key":"9174_CR32","doi-asserted-by":"crossref","first-page":"503","DOI":"10.1016\/0743-1066(94)90033-7","volume":"19","author":"J Jaffar","year":"1994","unstructured":"Jaffar, J., Maher, M.J.: Constraint logic programming: a survey. J. Log. Program. 19\/20, 503\u2013581 (1994)","journal-title":"J. Log. Program."},{"key":"9174_CR33","volume-title":"Partial evaluation and automatic program generation.","author":"ND Jones","year":"1993","unstructured":"Jones, N.D., Gomard, C.K., Sestoft, P.: Partial evaluation and automatic program generation. Prentice Hall, New York (1993)"},{"key":"9174_CR34","doi-asserted-by":"crossref","unstructured":"Komorovski, J.: An introduction to partial deduction. In: Meta Programming in Logic (META\u201992). Lecture Notes in Computer Science, vol.\u00a0649, pp.\u00a049\u201369. Springer, Heidelberg (1992)","DOI":"10.1007\/3-540-56282-6_4"},{"key":"9174_CR35","doi-asserted-by":"crossref","unstructured":"Kristiansen, L., Jones, N.D.: The flow of data and the complexity of algorithms. In: 1st Conference on Computability in Europe (CiE\u201905). Lecture Notes in Computer Science, vol.\u00a03526, pp.\u00a0263\u2013274 (2005)","DOI":"10.1007\/11494645_33"},{"issue":"2","key":"9174_CR36","doi-asserted-by":"crossref","first-page":"248","DOI":"10.1145\/42190.42347","volume":"10","author":"D Le Metayer","year":"1988","unstructured":"Le Metayer, D.: ACE: an automatic complexity evaluator. ACM Trans. Program. Lang. Syst. 10(2), 248\u2013266 (1988)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"3","key":"9174_CR37","doi-asserted-by":"crossref","first-page":"413","DOI":"10.1145\/982158.982159","volume":"26","author":"M Leuschel","year":"2004","unstructured":"Leuschel, M.: A framework for the integration of partial evaluation and abstract interpretation of logic programs. ACM Trans. Program. Lang. Syst. 26(3), 413\u2013463 (2004)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"4 & 5","key":"9174_CR38","doi-asserted-by":"crossref","first-page":"461","DOI":"10.1017\/S147106840200145X","volume":"2","author":"M Leuschel","year":"2002","unstructured":"Leuschel, M., Bruynooghe, M.: Logic program specialisation through partial deduction: control issues. Theory Pract. Log. Program. 2(4 & 5), 461\u2013515 (2002)","journal-title":"Theory Pract. Log. Program."},{"issue":"3\u20134","key":"9174_CR39","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1016\/0743-1066(91)90027-M","volume":"11","author":"JW Lloyd","year":"1991","unstructured":"Lloyd, J.W., Shepherdson, J.C.: Partial evaluation in logic programming. J. Log. Program. 11(3\u20134), 217\u2013242 (1991)","journal-title":"J. Log. Program."},{"key":"9174_CR40","doi-asserted-by":"crossref","unstructured":"Luca, B., Andrei, S., Anderson, H., Khoo, S.-C.: Program transformation by solving recurrences. In: ACM SIGPLAN Symposium on Partial Evaluation and Semantics-based Program Manipulation (PEPM \u201906), pp.\u00a0121\u2013129. ACM (2006)","DOI":"10.1145\/1111542.1111563"},{"issue":"4","key":"9174_CR41","first-page":"31","volume":"10","author":"J.-Y Marion","year":"2009","unstructured":"Marion, J.-Y., P\u00e9choux, R.: Sup-interpretations, a semantic method for static analysis of program resources. ACM Trans. Comput. Log. 10(4), 31 (2009) (Article 27)","journal-title":"ACM Trans. Comput. Log."},{"key":"9174_CR42","doi-asserted-by":"crossref","unstructured":"Navas, J., Mera, E., L\u00f3pez-Garc\u00eda, P., Hermenegildo, M.: User-definable resource bounds analysis for logic programs. In: 23rd International Conference on Logic Programming (ICLP\u201907), vol. 4670 of LNCS, pp.\u00a0348\u2013363. Springer, Heidelberg (2007)","DOI":"10.1007\/978-3-540-74610-2_24"},{"key":"9174_CR43","doi-asserted-by":"crossref","first-page":"106","DOI":"10.1145\/263699.263712","volume-title":"ACM Symposium on Principles of Programming Languages (POPL 1997)","author":"G Necula","year":"1997","unstructured":"Necula, G.: Proof-carrying code. In: ACM Symposium on Principles of Programming Languages (POPL 1997), pp.\u00a0106\u2013119. ACM Press, New York (1997)"},{"issue":"5","key":"9174_CR44","doi-asserted-by":"crossref","first-page":"1122","DOI":"10.1137\/S0097539704445597","volume":"35","author":"K-H Niggl","year":"2006","unstructured":"Niggl, K.-H., Wunderlich, H.: Certifying polynomial time and linear\/polynomial space for imperative programs. SIAM J. Comput. 35(5), 1122\u20131147 (2006)","journal-title":"SIAM J. Comput."},{"key":"9174_CR45","doi-asserted-by":"crossref","unstructured":"Podelski, A., Rybalchenko, A.: A complete method for the synthesis of linear ranking functions. In: 5th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI\u201904). Lecture Notes in Computer Science, pp.\u00a0239\u2013251. Springer, Heidelberg (2004)","DOI":"10.1007\/978-3-540-24622-0_20"},{"key":"9174_CR46","doi-asserted-by":"crossref","unstructured":"Puebla, G., Ochoa, C.: Poly-controlled partial evaluation. In: 8th ACM-SIGPLAN International Symposium on Principles and Practice of Declarative Programming (PPDP\u201906), pp.\u00a0261\u2013271. ACM Press, New York (2006)","DOI":"10.1145\/1140335.1140366"},{"key":"9174_CR47","doi-asserted-by":"crossref","unstructured":"Rosendahl, M.: Automatic complexity analysis. In: 4th ACM Conference on Functional Programming Languages and Computer Architecture (FPCA\u201989), pp.\u00a0144\u2013156. ACM Press (1989)","DOI":"10.1145\/99370.99381"},{"key":"9174_CR48","doi-asserted-by":"crossref","unstructured":"Rosendahl, M.: Simple driving techniques. In: Mogensen, T., Schmidt, D., Hal Sudborough, I. (eds.) The Essence of Computation. Lecture Notes in Computer Science, vol.\u00a02566, pp.\u00a0404\u2013419. Springer, Heidelberg (2002)","DOI":"10.1007\/3-540-36377-7_18"},{"issue":"4","key":"9174_CR49","doi-asserted-by":"crossref","first-page":"495","DOI":"10.1093\/logcom\/5.4.495","volume":"5","author":"D Sands","year":"1995","unstructured":"Sands, D.: A na\u00efve time analysis and its theory of cost equivalence. J. Log. Comput. 5(4), 495\u2013541 (1995)","journal-title":"J. Log. Comput."},{"issue":"4","key":"9174_CR50","doi-asserted-by":"crossref","first-page":"645","DOI":"10.1137\/0208051","volume":"8","author":"A Shamir","year":"1979","unstructured":"Shamir, A.: A linear time algorithm for finding minimum cutsets in reducible graphs. SIAM J. Comput. 8(4), 645\u2013655 (1979)","journal-title":"SIAM J. Comput."},{"key":"9174_CR51","unstructured":"Spoto, F., Hill, P.M., Payet, E.: Path-length analysis of object-oriented programs. In: 1st International Workshop on Emerging Applications of Abstract Interpretation (EAAI\u201906), Electronic Notes in Theoretical Computer Science. Elsevier, Amsterdam (2006)"},{"issue":"3","key":"9174_CR52","doi-asserted-by":"crossref","first-page":"292","DOI":"10.1145\/5956.5957","volume":"8","author":"VF Turchin","year":"1986","unstructured":"Turchin, V.F.: The concept of a supercompiler. ACM Trans. Program. Lang. Syst. 8(3), 292\u2013325 (1986)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"9174_CR53","doi-asserted-by":"crossref","unstructured":"Wadler, P.: Strictness analysis aids time analysis. In: ACM Symposium on Principles of Programming Languages (POPL\u201988), pp.\u00a0119\u2013132. ACM Press (1988)","DOI":"10.1145\/73560.73571"},{"issue":"9","key":"9174_CR54","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1145\/361002.361016","volume":"18","author":"B Wegbreit","year":"1975","unstructured":"Wegbreit, B.: Mechanical program analysis. Commun. ACM 18(9), 69\u201373 (1975)","journal-title":"Commun. ACM"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-010-9174-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-010-9174-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-010-9174-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T01:21:50Z","timestamp":1559265710000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-010-9174-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,4,29]]},"references-count":54,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2011,2]]}},"alternative-id":["9174"],"URL":"https:\/\/doi.org\/10.1007\/s10817-010-9174-1","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,4,29]]}}}