{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T19:36:52Z","timestamp":1725565012547},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642324949"},{"type":"electronic","value":"9783642324956"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-32495-6_3","type":"book-chapter","created":{"date-parts":[[2012,7,14]],"date-time":"2012-07-14T03:54:08Z","timestamp":1342238048000},"page":"36-53","source":"Crossref","is-referenced-by-count":3,"title":["Interpolation-Based Height Analysis for Improving a Recurrence Solver"],"prefix":"10.1007","author":[{"given":"Manuel","family":"Montenegro","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Olha","family":"Shkaravska","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marko","family":"van Eekelen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ricardo","family":"Pe\u00f1a","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"3_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/978-3-540-92188-2_5","volume-title":"Formal Methods for Components and Objects","author":"E. Albert","year":"2008","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: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2007. LNCS, vol.\u00a05382, pp. 113\u2013132. Springer, Heidelberg (2008)"},{"issue":"2","key":"3_CR2","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/s10817-010-9174-1","volume":"46","author":"E. Albert","year":"2011","unstructured":"Albert, E., Arenas, P., Genaim, S., Puebla, G.: Closed-form upper bounds in static cost analysis. J. Autom. Reasoning\u00a046(2), 161\u2013203 (2011)","journal-title":"J. Autom. Reasoning"},{"key":"3_CR3","doi-asserted-by":"crossref","unstructured":"Albert, E., Genaim, S., G\u00f3mez-Zamalloa, M.: Parametric inference of memory requirements for garbage collected languages. In: Vitek, J., Lea, D. (eds.) ISMM, pp. 121\u2013130. ACM (2010)","DOI":"10.1145\/1806651.1806671"},{"key":"3_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1007\/978-3-642-18275-4_5","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"E. Albert","year":"2011","unstructured":"Albert, E., Genaim, S., Masud, A.N.: More Precise Yet Widely Applicable Cost Analysis. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol.\u00a06538, pp. 38\u201353. Springer, Heidelberg (2011)"},{"key":"3_CR5","unstructured":"Bagnara, R., Zaccagnini, A., Zolo, T.: The automatic solution of recurrence relations. I. Linear recurrences of finite order with constant coefficients. Quaderno 334, Dipartimento di Matematica, Universit\u00e0 di Parma, Italy (2003), \n                    \n                      http:\/\/www.cs.unipr.it\/Publications\/"},{"key":"3_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/3-540-45789-5_17","volume-title":"Static Analysis","author":"R. Bagnara","year":"2002","unstructured":"Bagnara, R., Ricci, E., Zaffanella, E., Hill, P.M.: Possibly Not Closed Convex Polyhedra and the Parma Polyhedra Library. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol.\u00a02477, pp. 213\u2013229. Springer, Heidelberg (2002)"},{"key":"3_CR7","doi-asserted-by":"crossref","unstructured":"Brown, C.W.: QEPCAD: Quantifier Elimination by Partial Cylindrical Algebraic Decomposition (2004), \n                    \n                      http:\/\/www.cs.usna.edu\/qepcad\/B\/QEPCAD.html","DOI":"10.1145\/980175.980185"},{"key":"3_CR8","first-page":"23","volume-title":"Nonlinear and Convex Analysis, Proceedings in Honor of Ky Fan","author":"C.K. Chui","year":"1987","unstructured":"Chui, C.K., Lai, M.J.: Vandermonde determinants and lagrange interpolation in R\n                  \n                    s\n                  . In: Nonlinear and Convex Analysis, Proceedings in Honor of Ky Fan, pp. 23\u201335. Marcel Dekker Inc., N.Y. (1987)"},{"key":"3_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/3-540-07407-4_17","volume-title":"Automata Theory and Formal Languages","author":"G.E. Collins","year":"1975","unstructured":"Collins, G.E.: Quantifier Elimination for Real Closed Fields by Cylindrical Algebraic Decomposition. In: Brakhage, H. (ed.) GI-Fachtagung 1975. LNCS, vol.\u00a033, pp. 134\u2013183. Springer, Heidelberg (1975)"},{"key":"3_CR10","first-page":"91","volume":"7","author":"D.C. Cooper","year":"1972","unstructured":"Cooper, D.C.: Theorem proving in arithmetic without multiplication. Machine Intelligence\u00a07, 91\u2013100 (1972)","journal-title":"Machine Intelligence"},{"key":"3_CR11","unstructured":"Dolzmann, A., Sturm, T.: Redlog user manual. Tech. Rep. MIP-9905, FMI, Universit\u00e4t Passau, edition 2.0 for Version 2.0 (1999)"},{"key":"3_CR12","first-page":"36","volume-title":"Selected Revised Papers of the 8th International Symposium on Trends in Functional Programming (TFP 2007)","author":"M. Eekelen van","year":"2007","unstructured":"van Eekelen, M., Shkaravska, O., van Kesteren, R., Jacobs, B., Poll, E., Smetsers, S.: AHA: Amortized Heap space usage Analysis. In: Moraz\u00e1n, M. (ed.) Selected Revised Papers of the 8th International Symposium on Trends in Functional Programming (TFP 2007), pp. 36\u201353. Intellect, New York (2007)"},{"key":"3_CR13","unstructured":"Hearn, A.C.: REDUCE. User\u2019s Manual. Version 3.8 (2004)"},{"key":"3_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/978-3-642-11957-6_16","volume-title":"Programming Languages and Systems","author":"J. Hoffmann","year":"2010","unstructured":"Hoffmann, J., Hofmann, M.: Amortized Resource Analysis with Polynomial Potential. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol.\u00a06012, pp. 287\u2013306. Springer, Heidelberg (2010)"},{"key":"3_CR15","doi-asserted-by":"crossref","unstructured":"Hoffmann, J., Aehlig, K., Hofmann, M.: Multivariate amortized resource analysis. In: Ball, T., Sagiv, M. (eds.) POPL, pp. 357\u2013370. ACM (2011)","DOI":"10.1145\/1925844.1926427"},{"key":"3_CR16","doi-asserted-by":"crossref","unstructured":"Hofmann, M., Jost, S.: Static prediction of heap space usage for first-order functional programs. In: Proc. 30th ACM Symp. on Principles of Programming Languages, POPL 2003, pp. 185\u2013197. ACM Press (2003)","DOI":"10.1145\/640128.604148"},{"key":"3_CR17","doi-asserted-by":"crossref","unstructured":"van Kesteren, R., Shkaravska, O., van Eekelen, M.: Inferring static non-monotonically sized types through testing. In: Proceedings of 16th International Workshop on Functional and (Constraint) Logic Programming (WFLP 2007), Paris, France. ENTCS, vol.\u00a0216C, pp. 45\u201363 (2007)","DOI":"10.1016\/j.entcs.2008.06.033"},{"issue":"3","key":"3_CR18","doi-asserted-by":"publisher","first-page":"547","DOI":"10.1051\/ita:2005029","volume":"39","author":"S. Lucas","year":"2005","unstructured":"Lucas, S.: Polynomials over the reals in proofs of termination: from theory to practice. RAIRO Theoretical Informatics and Applications\u00a039(3), 547\u2013586 (2005)","journal-title":"RAIRO Theoretical Informatics and Applications"},{"issue":"2","key":"3_CR19","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/s10817-010-9183-0","volume":"45","author":"T. Nipkow","year":"2010","unstructured":"Nipkow, T.: Linear quantifier elimination. J. Autom. Reasoning\u00a045(2), 189\u2013212 (2010)","journal-title":"J. Autom. Reasoning"},{"key":"3_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/978-3-540-24622-0_20","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A. Podelski","year":"2004","unstructured":"Podelski, A., Rybalchenko, A.: A Complete Method for the Synthesis of Linear Ranking Functions. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol.\u00a02937, pp. 239\u2013251. Springer, Heidelberg (2004)"},{"issue":"2:10","key":"3_CR21","first-page":"1","volume":"5","author":"O. Shkaravska","year":"2009","unstructured":"Shkaravska, O., van Eekelen, M., van Kesteren, R.: Polynomial size analysis of first-order shapely functions. Logical Methods in Computer Science\u00a05(2:10), 1\u201335 (2009); selected Papers from TLCA 2007","journal-title":"Logical Methods in Computer Science"},{"key":"3_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"118","DOI":"10.1007\/978-3-642-24452-0_7","volume-title":"Implementation and Application of Functional Languages","author":"O. Shkaravska","year":"2011","unstructured":"Shkaravska, O., van Eekelen, M., Tamalet, A.: Collected Size Semantics for Functional Programs over Lists. In: Scholz, S.-B., Chitil, O. (eds.) IFL 2008. LNCS, vol.\u00a05836, pp. 118\u2013137. Springer, Heidelberg (2011)"},{"key":"3_CR23","doi-asserted-by":"crossref","unstructured":"Shkaravska, O., van Eekelen, M.C.J.D., van Kesteren, R.: Polynomial size analysis of first-order shapely functions. Logical Methods in Computer Science\u00a05(2) (2009)","DOI":"10.2168\/LMCS-5(2:10)2009"},{"key":"3_CR24","doi-asserted-by":"crossref","unstructured":"Shkaravska, O., Kersten, R., van Eekelen, M.: Test-based inference of polynomial loop-bound functions. In: Proceedings of the 8th International Conference on the Principles and Practice of Programming in Java, PPPJ 2010. ACM (2010)","DOI":"10.1145\/1852761.1852776"},{"key":"3_CR25","unstructured":"Tamalet, A., Shkaravska, O., van Eekelen, M.: Size analysis of algebraic data types. In: Achten, P., Koopman, P., Moraz\u00e1n, M.T. (eds.) Selected Revised Papers of the 9th International Symposium on Trends in Functional Programming (TFP 2008), pp. 33\u201348. Intellect (2009)"},{"key":"3_CR26","volume-title":"A Decision Method for Elementary Algebra and Geometry","author":"A. Tarski","year":"1948","unstructured":"Tarski, A.: A Decision Method for Elementary Algebra and Geometry. University of California Press, Berkeley (1948)"},{"issue":"9","key":"3_CR27","doi-asserted-by":"publisher","first-page":"528","DOI":"10.1145\/361002.361016","volume":"18","author":"B. Wegbreit","year":"1975","unstructured":"Wegbreit, B.: Mechanical program analysis. Commun. ACM\u00a018(9), 528\u2013539 (1975)","journal-title":"Commun. ACM"},{"issue":"1\/2","key":"3_CR28","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/S0747-7171(88)80003-8","volume":"5","author":"V. Weispfenning","year":"1988","unstructured":"Weispfenning, V.: The complexity of linear problems in fields. J. Symb. Comput.\u00a05(1\/2), 3\u201327 (1988)","journal-title":"J. Symb. Comput."}],"container-title":["Lecture Notes in Computer Science","Foundational and Practical Aspects of Resource Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-32495-6_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,3]],"date-time":"2019-05-03T22:02:08Z","timestamp":1556920928000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-32495-6_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642324949","9783642324956"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-32495-6_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}