{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T19:40:57Z","timestamp":1725565257690},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540223818"},{"type":"electronic","value":"9783540278153"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-27815-3_37","type":"book-chapter","created":{"date-parts":[[2010,9,14]],"date-time":"2010-09-14T04:32:16Z","timestamp":1284438736000},"page":"491-505","source":"Crossref","is-referenced-by-count":27,"title":["A Formally Verified Calculus for Full Java Card"],"prefix":"10.1007","author":[{"given":"Kurt","family":"Stenzel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"37_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-48737-9_1","volume-title":"Formal Syntax and Semantics of Java","year":"1999","unstructured":"Alves-Foss, J. (ed.): Formal Syntax and Semantics of Java. LNCS, vol.\u00a01523, p. 1. Springer, Heidelberg (1999)"},{"key":"37_CR2","series-title":"Lecture Notes in Computer Science","volume-title":"Java on Smart Cards: Programming and Security","year":"2001","unstructured":"Attali, I., Jensen, T. (eds.): JavaCard 2000. LNCS, vol.\u00a02041. Springer, Heidelberg (2001)"},{"key":"37_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/3-540-46428-X_25","volume-title":"Fundamental Approaches to Software Engineering","author":"M. Balser","year":"2000","unstructured":"Balser, M., Reif, W., Schellhorn, G., Stenzel, K., Thums, A.: Formal system development with KIV. In: Maibaum, T. (ed.) FASE 2000. LNCS, vol.\u00a01783, p. 363. Springer, Heidelberg (2000)"},{"key":"37_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"6","DOI":"10.1007\/3-540-45165-X_2","volume-title":"Java on Smart Cards: Programming and Security","author":"B. Beckert","year":"2001","unstructured":"Beckert, B.: A dynamic logic for the formal verification of java card programs. In: Attali, I., Jensen, T. (eds.) JavaCard 2000. LNCS, vol.\u00a02041, p. 6. Springer, Heidelberg (2001)"},{"key":"37_CR5","unstructured":"B\u00f6rger, E., Schulte, W.: A Programmer Friendly Modular Definition of the Semantics of Java. In: [1]"},{"key":"37_CR6","series-title":"Electronic Notes in Theoretical Computer Science","volume-title":"Proceedings FMICS 2003","author":"L. Burdy","year":"2003","unstructured":"Burdy, L., Cheon, Y., Cok, D., Ernst, M., Kiniry, J., Leavens, G., Leino, K., Poll, E.: An overview of JML tools and applications. In: Arts, T., Fokkink, W. (eds.) Proceedings FMICS 2003. Electronic Notes in Theoretical Computer Science, vol.\u00a080, Elsevier, Amsterdam (2003)"},{"key":"37_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45236-2_24","volume-title":"FME 2003: Formal Methods","author":"N. Burdy","year":"2003","unstructured":"Burdy, N., Requet, A., Lanet, J.-L.: Java applet correctness: A developeroriented approach. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol.\u00a02805, Springer, Heidelberg (2003)"},{"key":"37_CR8","doi-asserted-by":"crossref","unstructured":"Drossopoulou, S., Eisenbach, S.: Describing the Semantics of Java and Proving Type Soundness. In: [1]","DOI":"10.1007\/3-540-48737-9_2"},{"key":"37_CR9","unstructured":"In: Drossopoulou, S., Eisenbach, S., Jacobs, B., Leavens, G.T.,M\u00fcller, P., Poetzsch-Heffter, A. (eds.): Formal Techniques for Java Programs, Proceedings ECOOP 2000 Workshop. Technical Report 269, 5\/2000, Fernuniversit\u00e4t Hagen (2000)"},{"key":"37_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-09237-4","volume-title":"First-Order Dynamic Logic","author":"D. Harel","year":"1979","unstructured":"Harel, D.: First-Order Dynamic Logic. LNCS, vol.\u00a068. Springer, Heidelberg (1979)"},{"key":"37_CR11","doi-asserted-by":"crossref","unstructured":"Hartel, P., Moreau, L.: Formalizing the safety of Java, the Java virtual machine, and Java card. ACM Computing Surveys (CSUR)\u00a033(4) (December 2001)","DOI":"10.1145\/503112.503115"},{"key":"37_CR12","unstructured":"KIV home page, http:\/\/www.informatik.uni-augsburg.de\/swt\/fmg\/"},{"key":"37_CR13","unstructured":"Huisman, M.: Reasoning about JAVA programs in higher order logic with PVS and Isabelle. PhD thesis, University of Nijmegen, IPA dissertation series, 2001-03 (2001)"},{"key":"37_CR14","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, p. 284. Springer, Heidelberg (2000)"},{"key":"37_CR15","doi-asserted-by":"crossref","unstructured":"Jacobs, B., Leavens, G.T., M\u00fcller, P., Poetzsch-Heffter, A. (eds.): Formal Techniques for Java Programs. Technical Report 251, Fernuniversit\u00e4t Hagen (1999)","DOI":"10.1007\/3-540-46589-8_6"},{"key":"37_CR16","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: Hussmann, H. (ed.) FASE 2001. LNCS, vol.\u00a02029, p. 284. Springer, Heidelberg (2001)"},{"key":"37_CR17","doi-asserted-by":"crossref","unstructured":"Jacobs, B., Poll, E.: Java program verification at nijmegen: Developments and perspective. Technical Report NIII-R0318, University of Nijmegen (2003)","DOI":"10.1007\/978-3-540-37621-7_7"},{"key":"37_CR18","unstructured":"Java Card 2.2 Specification (2002), http:\/\/java.sun.com\/products\/javacard\/"},{"key":"37_CR19","volume-title":"The Java (tm) Language Specification","author":"B. Joy","year":"2000","unstructured":"Joy, B., Steele, G., Gosling, J., Bracha, G.: The Java (tm) Language Specification, 2nd edn. Addison-Wesley, Reading (2000)","edition":"2"},{"key":"37_CR20","unstructured":"KeY project homepage, http:\/\/i12www.ira.uka.de\/~key"},{"key":"37_CR21","unstructured":"Krakatoa home page, http:\/\/krakatoa.lri.fr\/"},{"key":"37_CR22","volume-title":"25th ACM Symposium on Principles of Programming Languages","author":"T. Nipkow","year":"1998","unstructured":"Nipkow, T., von Oheimb, D.: Java light is Type-Safe \u2013 Definitely. In: 25th ACM Symposium on Principles of Programming Languages, ACM, New York (1998)"},{"key":"37_CR23","volume-title":"Automated Deduction\u2014A Basis for Applications","author":"W. Reif","year":"1998","unstructured":"Reif, W., Schellhorn, G., Stenzel, K., Balser, M.: Structured specifications and interactive proofs with KIV. In: Bibel, W., Schmitt, P. (eds.) Automated Deduction\u2014A Basis for Applications, Kluwer Academic Publishers, Dordrecht (1998)"},{"key":"37_CR24","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-59495-3","volume-title":"Java and the Java Virtual Machine: Definition, Verification, Validation","author":"R.F. St\u00e4rk","year":"2001","unstructured":"St\u00e4rk, R.F., Schmid, J., B\u00f6rger, E.: Java and the Java Virtual Machine: Definition, Verification, Validation. Springer, Heidelberg (2001)"},{"key":"37_CR25","unstructured":"von Oheimb, D.: Analyzing Java in Isabelle\/HOL: Formalization, Type Safety and Hoare Logic. PhD thesis, Technische Universit\u00e4t M\u00fcnchen (2001)"},{"key":"37_CR26","unstructured":"von Oheimb, D., Nipkow, T.: Machine-checking the Java Specification: Proving Type-Safety. In: [1]"},{"key":"37_CR27","unstructured":"von Oheimb, D.: Axiomatic semantics for Java _ight in Isabelle\/HOL. In: [9]"}],"container-title":["Lecture Notes in Computer Science","Algebraic Methodology and Software Technology"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-27815-3_37.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T04:22:31Z","timestamp":1605759751000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-27815-3_37"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540223818","9783540278153"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-27815-3_37","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}