{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T01:39:40Z","timestamp":1725586780362},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642214363"},{"type":"electronic","value":"9783642214370"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-21437-0_16","type":"book-chapter","created":{"date-parts":[[2011,6,18]],"date-time":"2011-06-18T03:33:16Z","timestamp":1308367996000},"page":"184-199","source":"Crossref","is-referenced-by-count":2,"title":["Certification of Safe Polynomial Memory Bounds"],"prefix":"10.1007","author":[{"given":"Javier","family":"de Dios","sequence":"first","affiliation":[]},{"given":"Ricardo","family":"Pe\u00f1a","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"16_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/978-3-642-15769-1_8","volume-title":"Static Analysis","author":"C. Alias","year":"2010","unstructured":"Alias, C., Darte, A., Feautrier, P., Gonnord, L.: Multi-dimensional Rankings, Program Termination, and Complexity Bounds of Flowchart Programs. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol.\u00a06337, pp. 117\u2013133. Springer, Heidelberg (2010)"},{"key":"16_CR2","doi-asserted-by":"publisher","first-page":"411","DOI":"10.1016\/j.tcs.2007.09.003","volume":"389","author":"D. Aspinall","year":"2007","unstructured":"Aspinall, D., Beringer, L., Hofmann, M., Loidl, H.-W., Momigliano, A.: A program logic for resources. Theoretical Computer Science\u00a0389, 411\u2013445 (2007)","journal-title":"Theoretical Computer Science"},{"key":"16_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"218","DOI":"10.1007\/978-3-540-78800-3_16","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A.M. Ben-Amram","year":"2008","unstructured":"Ben-Amram, A.M., Codish, M.: A SAT-Based Approach to Size Change Termination with Global Ranking Functions. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 218\u2013232. Springer, Heidelberg (2008)"},{"key":"16_CR4","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1007\/978-3-540-32275-7_23","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"L. Beringer","year":"2005","unstructured":"Beringer, L., Hofmann, M., Momigliano, A., Shkaravska, O.: Automatic Certification of Heap Consumption. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS (LNAI), vol.\u00a03452, pp. 347\u2013362. Springer, Heidelberg (2005)"},{"key":"16_CR5","series-title":"An EATCS Series","volume-title":"Texts in Theoretical Computer Science","author":"Y. Bertot","year":"2004","unstructured":"Bertot, Y., Casteran, P.: Interactive Theorem Proving and Program Development Coq\u2019Art: The Calculus of Inductive Constructions. In: Texts in Theoretical Computer Science. An EATCS Series. Springer, Heidelberg (2004)"},{"key":"16_CR6","unstructured":"Bonfante, G., Marion, J.-Y., Moyen, J.-Y.: Quasi-interpretations. Technical Report, Loria (2004), http:\/\/www.loria.fr\/~moyen"},{"key":"16_CR7","doi-asserted-by":"crossref","unstructured":"Brown, C.\u00a0W.: QEPCAD: Quantifier Elimination by Partial Cylindrical Algebraic Decomposition (2004), http:\/\/www.cs.usna.edu\/qepcad\/B\/QEPCAD.html","DOI":"10.1145\/980175.980185"},{"key":"16_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/11526841_8","volume-title":"FM 2005: Formal Methods","author":"D. Cachera","year":"2005","unstructured":"Cachera, D., Jensen, T., Pichardie, D., Schneider, G.: Certified Memory Usage Analysis. In: Fitzgerald, J.S., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol.\u00a03582, pp. 91\u2013106. Springer, Heidelberg (2005)"},{"key":"16_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":"16_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"442","DOI":"10.1007\/3-540-45657-0_36","volume-title":"Computer Aided Verification","author":"M. Col\u00f3n","year":"2002","unstructured":"Col\u00f3n, M., Sipma, H.: Practical Methods for Proving Program Termination. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 442\u2013454. Springer, Heidelberg (2002)"},{"issue":"4","key":"16_CR11","first-page":"315","volume":"34","author":"E. Contejean","year":"2006","unstructured":"Contejean, E., March\u00e9, C., Tom\u00e1s, A.-P., Urbain, X.: Mechanically proving termination using polynomial interpretations. Journal of Automated Reasoning\u00a034(4), 315\u2013355 (2006)","journal-title":"Journal of Automated Reasoning"},{"key":"16_CR12","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. A Static Inference of Polynomial Bounds for Functional Programs. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol.\u00a06012, pp. 287\u2013306. Springer, Heidelberg (2010)"},{"key":"16_CR13","first-page":"185","volume-title":"Proc. 30th ACM Symp. on Principles of Programming Languages, POPL 2003","author":"M. Hofmann","year":"2003","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, New York (2003)"},{"key":"16_CR14","unstructured":"Lucas, S., Pe\u00f1a, R.: Rewriting Techniques for Analysing Termination and Complexity Bounds of SAFE Programs. In: LOPSTR 2008, Valencia, Spain, pp. 43\u201357 (2008)"},{"key":"16_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1007\/978-3-642-11999-6_10","volume-title":"Functional and Constraint Logic Programming","author":"M. Montenegro","year":"2010","unstructured":"Montenegro, M., Pe\u00f1a, R., Segura, C.: A Simple Region Inference Algorithm for a First-Order Functional Language. In: Escobar, S. (ed.) WFLP 2009. LNCS, vol.\u00a05979, pp. 145\u2013161. Springer, Heidelberg (2010)"},{"key":"16_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1007\/978-3-642-15331-0_3","volume-title":"Foundational and Practical Aspects of Resource Analysis","author":"M. Montenegro","year":"2010","unstructured":"Montenegro, M., Pe\u00f1a, R., Segura, C.: A space consumption analysis by abstract interpretation. In: van Eekelen, M., Shkaravska, O. (eds.) FOPARA 2009. LNCS, vol.\u00a06324, pp. 34\u201350. Springer, Heidelberg (2010)"},{"key":"16_CR17","first-page":"106","volume-title":"ACM SIGPLAN-SIGACT Principles of Programming Languages, POPL1997","author":"G.C. Necula","year":"1997","unstructured":"Necula, G.C.: Proof-Carrying Code. In: ACM SIGPLAN-SIGACT Principles of Programming Languages, POPL1997, pp. 106\u2013119. ACM Press, New York (1997)"},{"key":"16_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/3-540-45793-3_8","volume-title":"Computer Science Logic","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T.: Hoare Logics for Recursive Procedures and Unbounded Nondeterminism. In: Bradfield, J.C. (ed.) CSL 2002 and EACSL 2002. LNCS, vol.\u00a02471, pp. 103\u2013119. Springer, Heidelberg (2002)"},{"key":"16_CR19","series-title":"LNCS","volume-title":"Isabelle\/HOL. A Proof Assistant for Higher-Order Logic","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L., Wenzel, M.: Isabelle\/HOL. A Proof Assistant for Higher-Order Logic LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"16_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)"},{"key":"16_CR21","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)"}],"container-title":["Lecture Notes in Computer Science","FM 2011: Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-21437-0_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,11]],"date-time":"2019-06-11T20:07:16Z","timestamp":1560283636000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-21437-0_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642214363","9783642214370"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-21437-0_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}