{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T18:05:29Z","timestamp":1725559529876},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540278825"},{"type":"electronic","value":"9783540317142"}],"license":[{"start":{"date-parts":[[2005,1,1]],"date-time":"2005-01-01T00:00:00Z","timestamp":1104537600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11526841_8","type":"book-chapter","created":{"date-parts":[[2010,7,18]],"date-time":"2010-07-18T16:51:58Z","timestamp":1279471918000},"page":"91-106","source":"Crossref","is-referenced-by-count":22,"title":["Certified Memory Usage Analysis"],"prefix":"10.1007","author":[{"given":"David","family":"Cachera","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Jensen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Pichardie","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gerardo","family":"Schneider","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"3\u20134","key":"8_CR1","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1023\/B:JARS.0000021014.79255.33","volume":"31","author":"D. Aspinall","year":"2003","unstructured":"Aspinall, D., Compagnoni, A.: Heap bounded assembly language. Journal of Automated Reasoning\u00a031(3\u20134), 261\u2013302 (2003)","journal-title":"Journal of Automated Reasoning"},{"key":"8_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"302","DOI":"10.1007\/3-540-45309-1_20","volume-title":"Programming Languages and Systems","author":"G. Barthe","year":"2001","unstructured":"Barthe, G., Dufay, G., Jakubiec, L., Serpette, B., de Sousa, S.M.: A Formal Executable Semantics of the JavaCard Platform. In: Sands, D. (ed.) ESOP 2001. LNCS, vol.\u00a02028, p. 302. Springer, Heidelberg (2001)"},{"key":"8_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1007\/978-3-540-24725-8_27","volume-title":"Programming Languages and Systems","author":"D. Cachera","year":"2004","unstructured":"Cachera, D., Jensen, T., Pichardie, D., Rusu, V.: Extracting a data flow analyser in constructive logic. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol.\u00a02986, pp. 385\u2013400. Springer, Heidelberg (2004)"},{"key":"8_CR4","doi-asserted-by":"crossref","unstructured":"Casset, L., Burdy, L., Requet, A.: Formal Development of an embedded verifier for Java Card Byte Code. In: Proc.\u00a0of IEEE Int.\u00a0Conference on Dependable Systems & Networks (DSN) (2002)","DOI":"10.1007\/3-540-45614-7_17"},{"key":"8_CR5","first-page":"184","volume-title":"Proc.\u00a027th ACM Symp.\u00a0on Principles of Programming Languages (POPL 2000)","author":"K. Crary","year":"2000","unstructured":"Crary, K., Weirich, S.: Resource bound certification. In: Proc.\u00a027th ACM Symp.\u00a0on Principles of Programming Languages (POPL 2000), pp. 184\u2013198. ACM Press, New York (2000)"},{"key":"8_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/978-3-540-30482-1_10","volume-title":"Formal Methods and Software Engineering","author":"J.-C. Filli\u00e2tre","year":"2004","unstructured":"Filli\u00e2tre, J.-C., March\u00e9, C.: Multi-Prover Verification of C Programs. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol.\u00a03308, pp. 15\u201329. Springer, Heidelberg (2004)"},{"issue":"4","key":"8_CR7","first-page":"258","volume":"7","author":"M. Hofmann","year":"2000","unstructured":"Hofmann, M.: A type system for bounded space and functional in-place update. Nordic Journal of Computing\u00a07(4), 258\u2013289 (2000)","journal-title":"Nordic Journal of Computing"},{"key":"8_CR8","first-page":"185","volume-title":"Proc.\u00a0of 30th ACM Symp.\u00a0on 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.\u00a0of 30th ACM Symp.\u00a0on Principles of Programming Languages (POPL 2003), pp. 185\u2013197. ACM Press, New York (2003)"},{"issue":"3","key":"8_CR9","doi-asserted-by":"publisher","first-page":"583","DOI":"10.1016\/S0304-3975(02)00869-1","volume":"298","author":"G. Klein","year":"2002","unstructured":"Klein, G., Nipkow, T.: Verified Bytecode Verifiers. Theoretical Computer Science\u00a0298(3), 583\u2013626 (2002)","journal-title":"Theoretical Computer Science"},{"key":"8_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"150","DOI":"10.1007\/3-540-45418-7_13","volume-title":"Smart Card Programming and Security","author":"X. Leroy","year":"2001","unstructured":"Leroy, X.: On-card bytecode verification for Java card. In: Attali, S., Jensen, T. (eds.) E-smart 2001. LNCS, vol.\u00a02140, pp. 150\u2013164. Springer, Heidelberg (2001)"},{"key":"8_CR11","unstructured":"Marlet, R.: Syntax of the JCVM language to be studied in the SecSafe project. Technical Report SECSAFE-TL-005, Trusted Logic SA (May 2001)"},{"issue":"3","key":"8_CR12","doi-asserted-by":"publisher","first-page":"527","DOI":"10.1145\/319301.319345","volume":"21","author":"G. Morrisett","year":"1999","unstructured":"Morrisett, G., Walker, D., Crary, K., Glew, N.: From System F to typed assembly language. ACM Trans. Program. Lang. Syst.\u00a021(3), 527\u2013568 (1999)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"8_CR13","unstructured":"Pichardie, D.: Coq sources of the development, \n                    \n                      http:\/\/www.irisa.fr\/lande\/pichardie\/MemoryUsage\/"},{"key":"8_CR14","unstructured":"Schneider, G.: A constraint-based algorithm for analysing memory usage on Java cards. Technical Report RR-5440, INRIA (December 2004)"},{"key":"8_CR15","doi-asserted-by":"crossref","unstructured":"Siveroni, I.: Operational semantics of the Java Card Virtual Machine. J.\u00a0Logic and Algebraic Programming\u00a058(1-2) (2004)","DOI":"10.1016\/j.jlap.2003.07.003"}],"container-title":["Lecture Notes in Computer Science","FM 2005: Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11526841_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T20:14:42Z","timestamp":1558296882000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11526841_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540278825","9783540317142"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/11526841_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}