{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T19:56:42Z","timestamp":1725566202900},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540230175"},{"type":"electronic","value":"9783540301424"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-30142-4_3","type":"book-chapter","created":{"date-parts":[[2010,9,19]],"date-time":"2010-09-19T00:14:09Z","timestamp":1284855249000},"page":"34-49","source":"Crossref","is-referenced-by-count":13,"title":["A Program Logic for Resource Verification"],"prefix":"10.1007","author":[{"given":"David","family":"Aspinall","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lennart","family":"Beringer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Martin","family":"Hofmann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hans-Wolfgang","family":"Loidl","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alberto","family":"Momigliano","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":"682","DOI":"10.1007\/BFb0030634","volume-title":"TAPSOFT\u201997: Theory and Practice of Software Development","author":"M. Abadi","year":"1997","unstructured":"Abadi, M., Leino, R.: A Logic of Object-Oriented Programs. In: Bidoit, M., Dauchet, M. (eds.) TAPSOFT 1997. LNCS, vol.\u00a01214, pp. 682\u2013696. Springer, Heidelberg (1997)"},{"key":"3_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-39656-7_1","volume-title":"Formal Methods for Components and Objects","author":"E. \u00c1brah\u00e1m","year":"2003","unstructured":"\u00c1brah\u00e1m, E., de Boer, F.S., de Roever, W.-P., Steffen, M.: A tool-supported proof system for multithreaded java. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2002. LNCS, vol.\u00a02852, pp. 1\u201332. Springer, Heidelberg (2003)"},{"key":"3_CR3","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":"3_CR4","doi-asserted-by":"crossref","unstructured":"Beringer, L., MacKenzie, K., Stark, I.: Grail: a Functional Form for Imperative Mobile Code. Electronic Notes in Theoretical Computer Science\u00a085(1) (2003)","DOI":"10.1016\/S1571-0661(05)80083-0"},{"key":"3_CR5","series-title":"IFIP Conference Proceedings","first-page":"163","volume-title":"FMOODS 2002","author":"F.D. Boer","year":"2002","unstructured":"Boer, F.D., Pierik, C.: Computer-aided specification and verification of annotated objectoriented programs. In: Jacobs, B., Rensink, A. (eds.) FMOODS 2002. IFIP Conference Proceedings, vol.\u00a0209, pp. 163\u2013177. Kluwer, Dordrecht (2002)"},{"key":"3_CR6","unstructured":"Burdy, L., Requet, A.: Jack: Java applet correctness kit. In: 4th Gemplus Developer Conference (2002)"},{"key":"3_CR7","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1145\/349299.349315","volume-title":"PLDI 2000 \u2013 Conference on Programming Language Design and Implementation","author":"C. Colby","year":"2000","unstructured":"Colby, C., Lee, P., Necula, G., Blau, F., Plesko, M., Cline, K.: A Certifying Compiler for Java. In: PLDI 2000 \u2013 Conference on Programming Language Design and Implementation, pp. 95\u2013107. ACM Press, New York (2000)"},{"key":"3_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/3-540-49019-1_10","volume-title":"Foundations of Software Science and Computation Structures","author":"F. Boer de","year":"1999","unstructured":"de Boer, F.: A WP-calculus for OO. In: Thomas, W. (ed.) FOSSACS 1999. LNCS, vol.\u00a01578, pp. 135\u2013149. Springer, Heidelberg (1999)"},{"key":"3_CR9","unstructured":"Filli\u00e2tre, J.-C.: Why: a multi-language multi-prover verification tool. Research Report 1366, LRI, Universit\u00e9 Paris Sud (March 2003), \n                  \n                    http:\/\/www.lri.fr\/filliatr\/ftp\/publis\/why-tool.ps.gz"},{"key":"3_CR10","unstructured":"Hofmann, M.: Semantik und Verifikation. Lecture Notes, WS 97\/98. TU Darmstadt (1998)"},{"issue":"4","key":"3_CR11","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":"Journal of Computing"},{"key":"3_CR12","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1145\/604131.604148","volume-title":"POPL 2003 \u2013 Symposium on Principles of Programming Languages","author":"M. Hofmann","year":"2003","unstructured":"Hofmann, M., Jost, S.: Static Prediction of Heap Space Usage for First-Order Functional Programs. In: POPL 2003 \u2013 Symposium on Principles of Programming Languages, New Orleans, LA, USA, January 2003, pp. 185\u2013197. ACM Press, New York (2003)"},{"key":"3_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1007\/3-540-46428-X_20","volume-title":"Fundamental Approaches to Software Engineering","author":"M. Huisman","year":"2000","unstructured":"Huisman, M., Jacobs, B.: Java Program Verification via a Hoare Logic with Abrupt Termination. In: Maibaum, T. (ed.) FASE 2000. LNCS, vol.\u00a01783, pp. 284\u2013303. Springer, Heidelberg (2000)"},{"key":"3_CR14","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":"3_CR15","unstructured":"Kleymann, T.: Hoare Logic and VDM: Machine-Checked Soundness and Completeness Proofs. PhD thesis, LFCS, University of Edinburgh (1999)"},{"issue":"4","key":"3_CR16","first-page":"330","volume":"5","author":"R. Leino","year":"1998","unstructured":"Leino, R.: Recursive Object Types in a Logic of Object-oriented Programs. Nordic Journal of Computing\u00a05(4), 330\u2013360 (1998)","journal-title":"Nordic Journal of Computing"},{"key":"3_CR17","unstructured":"MacKenzie, K., Wolverson, N.: Camelot and Grail: Compiling a Resource-aware Functional Language for the Java Virtual Machine. In: TFP 2003, Symposium on Trends in Functional Languages, Edinburgh, September 11-12 (2003)"},{"key":"3_CR18","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1016\/j.jlap.2003.07.006","volume":"58","author":"C. Marche","year":"2004","unstructured":"Marche, C., Paulin-Mohring, C., Urbain, X.: The KRAKATOA tool for certification of JAVA\/JAVACARD programs annotated in JML. Journal of Logic and Algebraic Programming\u00a058, 89 (2004)","journal-title":"Journal of Logic and Algebraic Programming"},{"key":"3_CR19","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":"3_CR20","unstructured":"Meyer, J., M\u00fcller, P., Poetzsch-Heffter, A.: The JIVE system\u2013implementation description (2000); available from \n                  \n                    www.informatik.fernuni-hagen.de\/pi5\/publications.html"},{"key":"3_CR21","first-page":"227","volume":"191","author":"J.S. Moore","year":"2003","unstructured":"Moore, J.S.: Proving theorems about Java and the JVM with ACL2. NATO Science Series Sub Series III Computer and Systems Sciences\u00a0191, 227\u2013290 (2003)","journal-title":"NATO Science Series Sub Series III Computer and Systems Sciences"},{"key":"3_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/3-540-49099-X_11","volume-title":"Programming Languages and Systems","author":"P. M\u00fcller","year":"1999","unstructured":"M\u00fcller, P., Poetzsch-Heffter, A.: A Programming Logic for Sequential Java. In: Swierstra, S.D. (ed.) ESOP 1999. LNCS, vol.\u00a01576, pp. 162\u2013176. Springer, Heidelberg (1999)"},{"key":"3_CR23","doi-asserted-by":"publisher","first-page":"106","DOI":"10.1145\/263699.263712","volume-title":"POPL 1997 \u2013 Symposium on Principles of Programming Languages","author":"G. Necula","year":"1997","unstructured":"Necula, G.: Proof-carrying Code. In: POPL 1997 \u2013 Symposium on Principles of Programming Languages, Paris, France, January 15\u201317, pp. 106\u2013116. ACM Press, New York (1997)"},{"key":"3_CR24","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":"3_CR25","unstructured":"Pierik, C., Boer, F.d.: A rule of adaptation for OO. Technical Report UU-CS-2003-032, Utrecht University (2004)"},{"key":"3_CR26","doi-asserted-by":"crossref","unstructured":"Reynolds, J.: Separation Logic: A Logic for Shared Mutable Data Structures. In: LICS 2002 \u2013 Symposium on Logic in Computer Science, Copenhagen, Denmark, July 22\u201325 (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"key":"3_CR27","unstructured":"Sannella, D., Hofmann, M.: Mobile Resource Guarantees. EU OpenFET Project (2002), \n                  \n                    http:\/\/www.dcs.ed.ac.uk\/home\/mrg\/"},{"key":"3_CR28","unstructured":"Tang, F.: Towards feasible, machine assisted verification of object-oriented programs. PhD thesis, School of Informatics, University of Edinburgh (2002)"},{"issue":"13","key":"3_CR29","doi-asserted-by":"publisher","first-page":"1173","DOI":"10.1002\/cpe.598","volume":"13","author":"D. Oheimb von","year":"2001","unstructured":"von Oheimb, D.: Hoare logic for Java in Isabelle\/HOL. Concurrency and Computation: Practice and Experience\u00a013(13), 1173\u20131214 (2001)","journal-title":"Concurrency and Computation: Practice and Experience"}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-30142-4_3.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,3]],"date-time":"2021-05-03T03:52:18Z","timestamp":1620013938000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-30142-4_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540230175","9783540301424"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-30142-4_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}