{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T20:29:52Z","timestamp":1761596992520},"publisher-location":"Berlin, Heidelberg","reference-count":32,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540489375"},{"type":"electronic","value":"9783540489382"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11924661_24","type":"book-chapter","created":{"date-parts":[[2006,10,27]],"date-time":"2006-10-27T09:42:39Z","timestamp":1161942159000},"page":"389-405","source":"Crossref","is-referenced-by-count":9,"title":["A Bytecode Logic for JML and Types"],"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"}]}],"member":"297","reference":[{"issue":"2-3","key":"24_CR1","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1016\/j.tcs.2004.09.019","volume":"331","author":"E. \u00c1brah\u00e1m","year":"2005","unstructured":"\u00c1brah\u00e1m, E., de Boer, F.S., de Roever, W.P., Steffen, M.: An assertion-based proof system for multithreaded Java. Theoretical Computer Science\u00a0331(2-3), 251\u2013290 (2005)","journal-title":"Theoretical Computer Science"},{"key":"24_CR2","volume-title":"Proceedings of the 11th ACM International Conference on Functional Programming (ICFP 2006)","author":"L.B.A. Nanevski","year":"2006","unstructured":"Nanevski, L.B.A., Morrisett, G.: Polymorphism and Separation in Hoare Type Theory. In: Proceedings of the 11th ACM International Conference on Functional Programming (ICFP 2006). ACM Press, New York (2006)"},{"issue":"4","key":"24_CR3","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1145\/278283.278285","volume":"33","author":"A.W. Appel","year":"1998","unstructured":"Appel, A.W.: SSA is functional programming. ACM SIGPLAN Notices\u00a033(4), 17\u201320 (1998)","journal-title":"ACM SIGPLAN Notices"},{"key":"24_CR4","volume-title":"Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science (LICS)","author":"A.W. Appel","year":"2001","unstructured":"Appel, A.W.: Foundational proof-carrying code. In: Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science (LICS). IEEE Computer Society, Los Alamitos (2001)"},{"key":"24_CR5","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":"24_CR6","series-title":"ENTCS","volume-title":"Proceedings of the 5th International Workshop on Compiler Optimization Meets Compiler Verification (COCV 2006)","author":"D. Aspinall","year":"2006","unstructured":"Aspinall, D., Beringer, L., Momigliano, A.: Optimisation validation. In: Knoop, J., Necula, G.C., Zimmermann, W. (eds.) Proceedings of the 5th International Workshop on Compiler Optimization Meets Compiler Verification (COCV 2006). ENTCS. Elsevier, Amsterdam (to appear, 2006)"},{"key":"24_CR7","series-title":"ENTCS","first-page":"255","volume-title":"Bytecode Semantics, Verification, Analysis and Transformation (BYTECODE)","author":"F.Y. Bannwart","year":"2005","unstructured":"Bannwart, F.Y., M\u00fcller, P.: A logic for bytecode. In: Spoto, F. (ed.) Bytecode Semantics, Verification, Analysis and Transformation (BYTECODE). ENTCS, vol.\u00a0141(1), pp. 255\u2013273. Elsevier, Amsterdam (2005)"},{"key":"24_CR8","unstructured":"Barthe, G.: Mobius \u2013 Mobility, Ubiquity and Security, http:\/\/mobius.inria.fr"},{"key":"24_CR9","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"626","DOI":"10.1007\/3-540-45744-5_51","volume-title":"Automated Reasoning","author":"B. Beckert","year":"2001","unstructured":"Beckert, B., Schlager, S.: A sequent calculus for first-order dynamic logic with trace modalities. In: Gor\u00e9, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol.\u00a02083, pp. 626\u2013641. Springer, Heidelberg (2001)"},{"key":"24_CR10","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1145\/964001.964003","volume-title":"Proceedings of the 31st ACM Symposium on Principles of Programming Languages, POPL 2004","author":"N. Benton","year":"2004","unstructured":"Benton, N.: Simple relational correctness proofs for static analyses and program transformations. In: Jones, N.D., Leroy, X. (eds.) Proceedings of the 31st ACM Symposium on Principles of Programming Languages, POPL 2004, Venice, Italy, pp. 14\u201325. ACM, New York (2004)"},{"key":"24_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11575467_24","volume-title":"Programming Languages and Systems","author":"N. Benton","year":"2005","unstructured":"Benton, N.: A typed, compositional logic for a stack-based abstract machine. In: Yi, K. (ed.) APLAS 2005. LNCS, vol.\u00a03780, pp. 364\u2013380. Springer, Heidelberg (2005)"},{"key":"24_CR12","doi-asserted-by":"crossref","unstructured":"Beringer, L., Hofmann, M.: A bytecode logic for JML and types \u2013 Isabelle\/HOL sources (2006), http:\/\/www.tcs.ifi.lmu.de\/~beringer\/BytecodeLogic.tar.gz","DOI":"10.1007\/11924661_24"},{"key":"24_CR13","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)"},{"issue":"3","key":"24_CR14","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1007\/s10009-004-0167-4","volume":"7","author":"L. Burdy","year":"2005","unstructured":"Burdy, L., Cheon, Y., Cok, D., Ernst, M., Kiniry, J., Leavens, G.T., Leino, K.R.M., Poll, E.: An overview of JML tools and applications. International Journal on Software Tools for Technology Transfer\u00a07(3), 212\u2013232 (2005)","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"24_CR15","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.P., 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":"24_CR16","doi-asserted-by":"crossref","unstructured":"Cytron, R., Ferrante, J., Rosen, B.K., Wegman, M.N., Zadeck, F.K.: Efficiently computing static single assignment form and the control dependence graph. ACM Transactions on Programming Languages and Systems (TOPLAS)\u00a013(4) (October 1991)","DOI":"10.1145\/115372.115320"},{"key":"24_CR17","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1145\/512529.512558","volume-title":"PLDI 2002: Proceedings of the ACM Conference on Programming language design and implementation","author":"C. Flanagan","year":"2002","unstructured":"Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for java. In: PLDI 2002: Proceedings of the ACM Conference on Programming language design and implementation, pp. 234\u2013245. ACM Press, New York (2002)"},{"key":"24_CR18","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1145\/155090.155113","volume-title":"PLDI 1993: Proceedings of the ACM Conference on Programming language design and implementation","author":"C. Flanagan","year":"1993","unstructured":"Flanagan, C., Sabry, A., Duba, B.F., Felleisen, M.: The essence of compiling with continuations. In: PLDI 1993: Proceedings of the ACM Conference on Programming language design and implementation, pp. 237\u2013247. ACM Press, New York (1993)"},{"key":"24_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/978-3-540-30569-9_8","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"R. H\u00e4hnle","year":"2005","unstructured":"H\u00e4hnle, R., Mostowski, W.: Verification of safety properties in the presence of transactions. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol.\u00a03362, pp. 151\u2013171. Springer, Heidelberg (2005)"},{"key":"24_CR20","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1145\/604131.604148","volume-title":"POPL 2003: Proceedings of the 30th ACM 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: Proceedings of the 30th ACM Symposium on Principles of programming languages, pp. 185\u2013197. ACM Press, New York (2003)"},{"key":"24_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1007\/3-540-45314-8_21","volume-title":"Fundamental Approaches to Software Engineering","author":"B. Jacobs","year":"2001","unstructured":"Jacobs, B., Poll, E.: A logic for the java modeling language JML. In: Hu\u00dfmann, H. (ed.) FASE 2001. LNCS, vol.\u00a02029, pp. 284\u2013299. Springer, Heidelberg (2001)"},{"key":"24_CR22","volume-title":"Systematic Software Development Using VDM","author":"C.B. Jones","year":"1990","unstructured":"Jones, C.B.: Systematic Software Development Using VDM, 2nd edn. Prentice-Hall, Englewood Cliffs (1990)","edition":"2"},{"issue":"3","key":"24_CR23","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1145\/202530.202532","volume":"30","author":"R.A. Kelsey","year":"1995","unstructured":"Kelsey, R.A.: A correspondence between continuation passing style and static single assignment form. ACM SIGPLAN Notices\u00a030(3), 13\u201322 (1995)","journal-title":"ACM SIGPLAN Notices"},{"key":"24_CR24","unstructured":"Kleymann, T.: Hoare Logic and VDM: Machine-Checked Soundness and Completeness Proofs. PhD thesis, LFCS, University of Edinburgh (1998)"},{"key":"24_CR25","unstructured":"Leavens, G.T., Poll, E., Clifton, C., Cheon, Y., Ruby, C., Cok, D., M\u00fcller, P., Kiniry, J.: JML Reference Manual (draft) (May 2006), http:\/\/www.cs.iastate.edu\/~leavens\/JML"},{"key":"24_CR26","unstructured":"Leino, K.R.M., Stata, R.: Checking object invariants. Technical Report #1997-007, Digital Equipment Corporation Systems Research Center, Palo Alto, USA (1997)"},{"key":"24_CR27","unstructured":"Nanevski, A., Morrisett, G.: Dependent type theory of stateful higher-order functions. Technical Report TR-24-05, Harvard University (2005)"},{"key":"24_CR28","doi-asserted-by":"publisher","first-page":"106","DOI":"10.1145\/263699.263712","volume-title":"POPL 1997: Proceedings of the 24th ACM Symposium on Principles of programming languages","author":"G.C. Necula","year":"1997","unstructured":"Necula, G.C.: Proof-carrying code. In: POPL 1997: Proceedings of the 24th ACM Symposium on Principles of programming languages, pp. 106\u2013119. ACM Press, New York (1997)"},{"key":"24_CR29","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":"24_CR30","unstructured":"Pichardie, D.: Bicolano \u2013 Byte Code Language in Coq (2006), http:\/\/www-sop.inria.fr\/everest\/personnel\/David.Pichardie\/bicolano\/main.html"},{"key":"24_CR31","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1109\/LICS.2002.1029817","volume-title":"Proceedings of the 17th IEEE Symposium on Logic in Computer Science (LICS 2002).","author":"J.C. Reynolds","year":"2002","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Proceedings of the 17th IEEE Symposium on Logic in Computer Science (LICS 2002)., pp. 55\u201374. IEEE Computer Society, Los Alamitos (2002)"},{"key":"24_CR32","unstructured":"Rinard, M., Marinov, D.: Credible compilation with pointers. In: Proceedings of the FLoC Workshop on Run-Time Result Verification (July 1999)"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11924661_24.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T14:59:41Z","timestamp":1605625181000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11924661_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540489375","9783540489382"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/11924661_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}