{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T20:34:04Z","timestamp":1761597244754},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540252368"},{"type":"electronic","value":"9783540322757"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/978-3-540-32275-7_23","type":"book-chapter","created":{"date-parts":[[2010,12,20]],"date-time":"2010-12-20T21:14:41Z","timestamp":1292879681000},"page":"347-362","source":"Crossref","is-referenced-by-count":17,"title":["Automatic Certification of Heap Consumption"],"prefix":"10.1007","author":[{"given":"Lennart","family":"Beringer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Martin","family":"Hofmann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alberto","family":"Momigliano","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Olha","family":"Shkaravska","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"23_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1007\/978-3-540-30142-4_3","volume-title":"Theorem Proving in Higher Order Logics","author":"D. Aspinall","year":"2004","unstructured":"Aspinall, D., Beringer, L., Hofmann, M., Loidl, H.-W., Momigliano, A.: A program logic for resource verification. In: Slind, K., Bunker, A., Gopalakrishnan, G.C. (eds.) TPHOLs 2004. LNCS, vol.\u00a03223, pp. 34\u201349. Springer, Heidelberg (2004)"},{"key":"23_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1007\/3-540-45927-8_4","volume-title":"Programming Languages and Systems","author":"D. Aspinall","year":"2002","unstructured":"Aspinall, D., Hofmann, M.: Another type system for in-place update. In: Le M\u00e9tayer, D. (ed.) ESOP 2002. LNCS, vol.\u00a02305, pp. 36\u201352. Springer, Heidelberg (2002)"},{"key":"23_CR3","unstructured":"Beringer, L., Hofmann, M., Momigliano, A., Shkaravska, O.: Towards certificate generation for linear heap consumption. In: Proceedings of LRPP 2004 (July 2004)"},{"key":"23_CR4","series-title":"Electronic Notes in Theoretical Computer Science","volume-title":"Proceedings FGC 03","author":"L. Beringer","year":"2003","unstructured":"Beringer, L., MacKenzie, K., Stark, I.: Grail: a Functional Form for Imperative Mobile Code. In: Proceedings FGC 03, June 2003. Electronic Notes in Theoretical Computer Science, vol.\u00a085(1), Elsevier, Amsterdam (2003)"},{"key":"23_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/10722010_8","volume-title":"Mathematics of Program Construction","author":"R. Bornat","year":"2000","unstructured":"Bornat, R.: Proving Pointer Programs in Hoare Logic. In: Backhouse, R., Oliveira, J.N. (eds.) MPC 2000. LNCS, vol.\u00a01837, pp. 102\u2013126. Springer, Heidelberg (2000)"},{"key":"23_CR6","first-page":"185","volume-title":"Proceedings of POPL 2003","author":"M. Hofmann","year":"2003","unstructured":"Hofmann, M., Jost, S.: Static prediction of heap space usage for first-order functional programs. In: Proceedings of POPL 2003, January 2003, pp. 185\u2013197. ACM Press, New York (2003)"},{"key":"23_CR7","volume-title":"Systematic Software Development Using VDM","author":"C. Jones","year":"1990","unstructured":"Jones, C.: Systematic Software Development Using VDM. Prentice-Hall, Englewood Cliffs (1990)"},{"key":"23_CR8","unstructured":"Kleymann, T.: Hoare Logic and VDM: Machine-Checked Soundness and Completeness Proofs. PhD thesis, LFCS, University of Edinburgh (1999)"},{"key":"23_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/3-540-44904-3_14","volume-title":"Typed Lambda Calculi and Applications","author":"M. Kone\u010dn\u00fd","year":"2003","unstructured":"Kone\u010dn\u00fd, M.: Functional in-place update with layered datatype sharing. In: Hofmann, M.O. (ed.) TLCA 2003. LNCS, vol.\u00a02701, pp. 195\u2013210. Springer, Heidelberg (2003)"},{"key":"23_CR10","unstructured":"Leino, K.R.M.: Toward Reliable Modular Programs. PhD thesis, California Institute of Technology (1995) Available as Technical Report Caltech-CS-TR-95-03"},{"issue":"2","key":"23_CR11","doi-asserted-by":"publisher","first-page":"226","DOI":"10.1145\/357073.357078","volume":"1","author":"D.C. Luckham","year":"1979","unstructured":"Luckham, D.C., Suzuki, N.: Verification of array, record, and pointer operations in Pascal. ACM Transactions on Programming Languages and Systems\u00a01(2), 226\u2013244 (1979)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"23_CR12","doi-asserted-by":"crossref","unstructured":"MacKenzie, K., Wolverson, N.: Camelot and Grail: Resource-aware Functional Programming on the JVM. In: Gilmore, S. (ed.) Proceedings of TFP 2003, intellect, pp. 29\u201346 (2003)","DOI":"10.2307\/j.ctv36xvxxx.6"},{"key":"23_CR13","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/978-3-540-45085-6_10","volume-title":"Automated Deduction \u2013 CADE-19","author":"F. Mehta","year":"2003","unstructured":"Mehta, F., Nipkow, T.: Proving pointer programs in higher-order logic. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol.\u00a02741, pp. 121\u2013135. Springer, Heidelberg (2003)"},{"key":"23_CR14","doi-asserted-by":"publisher","first-page":"106","DOI":"10.1145\/263699.263712","volume-title":"Proceedings of POPL 1997","author":"G.C. Necula","year":"1997","unstructured":"Necula, G.C.: Proof-carrying code. In: Proceedings of POPL 1997, pp. 106\u2013119. ACM Press, New York (1997)"},{"key":"23_CR15","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":"23_CR16","volume-title":"Proceedings of LICS 2002","author":"J. Reynolds","year":"2002","unstructured":"Reynolds, J.: Separation Logic: A Logic for Shared Mutable Data Structures. In: Proceedings of LICS 2002, July 2002, IEEE Computer Society, Los Alamitos (2002)"},{"key":"23_CR17","unstructured":"Sannella, D., Hofmann, M.: Mobile Resource Guarantees. EU Project IST-2001-33149 (2002\u20132004), http:\/\/groups\/inf.ed.ac.uk\/mrg\/"},{"key":"23_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1007\/978-3-540-30124-0_21","volume-title":"Computer Science Logic","author":"T. Weber","year":"2004","unstructured":"Weber, T.: Towards mechanized program verification with separation logic. In: Marcinkowski, J., Tarlecki, A. (eds.) CSL 2004. LNCS, vol.\u00a03210, pp. 250\u2013264. Springer, Heidelberg (2004)"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-32275-7_23.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,4]],"date-time":"2023-06-04T15:26:27Z","timestamp":1685892387000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-32275-7_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540252368","9783540322757"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-32275-7_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}