{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T06:00:38Z","timestamp":1725516038518},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540799795"},{"type":"electronic","value":"9783540799801"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-79980-1_24","type":"book-chapter","created":{"date-parts":[[2008,7,28]],"date-time":"2008-07-28T15:55:42Z","timestamp":1217260542000},"page":"315-329","source":"Crossref","is-referenced-by-count":2,"title":["Verification of Java Programs with Generics"],"prefix":"10.1007","author":[{"given":"Kurt","family":"Stenzel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Holger","family":"Grandy","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wolfgang","family":"Reif","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"24_CR1","series-title":"Lecture Notes in Computer Science","volume-title":"Formal Syntax and Semantics of Java","year":"1999","unstructured":"Alves-Foss, J. (ed.): Formal Syntax and Semantics of Java. LNCS, vol.\u00a01523. Springer, Heidelberg (1999)"},{"key":"24_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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. Springer, Heidelberg (2000)"},{"key":"24_CR3","series-title":"Lecture Notes in Computer Science","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"M. Barnett","year":"2005","unstructured":"Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: An Overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol.\u00a03362. Springer, Heidelberg (2005)"},{"key":"24_CR4","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74792-5_7","volume-title":"FMCO: Proceedings of 5th International Symposium on Formal Methods for Components and Objects","author":"G. Barthe","year":"2007","unstructured":"Barthe, G., Burdy, L., Charles, J., Gr\u00e9goire, B., Huisman, M., Lanet, J.-L., Pavlova, M., Requet, A.: JACK: a tool for validation of security and behaviour of Java applications. In: FMCO: Proceedings of 5th International Symposium on Formal Methods for Components and Objects, vol.\u00a04709. Springer, Heidelberg (2007)"},{"key":"24_CR5","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Verification of Object-Oriented Software. The KeY Approach","year":"2007","unstructured":"Beckert, B., H\u00e4hnle, R., Schmitt, P. (eds.): Verification of Object-Oriented Software. LNCS (LNAI), vol.\u00a04334. Springer, Heidelberg (2007)"},{"key":"24_CR6","doi-asserted-by":"crossref","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) (2005)","DOI":"10.1007\/s10009-004-0167-4"},{"key":"24_CR7","series-title":"Lecture Notes in Computer Science","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"D.R. Cok","year":"2005","unstructured":"Cok, D.R., Kiniry, J.R.: ESC\/Java2: Uniting ESC\/Java and JML. In: Barthe, G., Huisman, M. (eds.) CASSIS 2004. LNCS, vol.\u00a03362. Springer, Heidelberg (2005)"},{"key":"24_CR8","volume-title":"The Java Language Specification","author":"J. Gosling","year":"1996","unstructured":"Gosling, J., Joy, B., Steele, G.: The Java Language Specification. Addison-Wesley, Reading (1996)"},{"key":"24_CR9","volume-title":"The Java (tm) Language Specification","author":"J. Gosling","year":"2005","unstructured":"Gosling, J., Joy, B., Steele, G., Bracha, G.: The Java (tm) Language Specification, 3rd edn. Addison-Wesley, Reading (2005)","edition":"3"},{"key":"24_CR10","volume-title":"Software Engineering and Formal Methods, SEFM","author":"H. Grandy","year":"2007","unstructured":"Grandy, H., Bertossi, R., Stenzel, K., Reif, W.: ASN1-light: A Verified Message Encoding for Security Protocols. In: Software Engineering and Formal Methods, SEFM. IEEE Press, Los Alamitos (2007)"},{"key":"24_CR11","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-68237-0_13","volume-title":"FM 2008: 15th Int.\u00a0Symposium on Formal Methods","author":"H. Grandy","year":"2008","unstructured":"Grandy, H., Bischof, M., Schellhorn, G., Reif, W., Stenzel, K.: Verification of Mondex Electronic Purses with KIV: From a Security Protocol to Verified Code. In: FM 2008: 15th Int.\u00a0Symposium on Formal Methods, vol.\u00a05014. Springer, Heidelberg (2008)"},{"key":"24_CR12","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/2516.001.0001","volume-title":"Dynamic Logic","author":"D. Harel","year":"2000","unstructured":"Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press, Cambridge (2000)"},{"key":"24_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/b101561","volume-title":"Algebraic Methodology and Software Technology","author":"B. Jacobs","year":"2004","unstructured":"Jacobs, B., March\u00e9, C., Rauch, N.: Formal verification of a commercial smart card applet with multiple tools. In: Rattray, C., Maharaj, S., Shankland, C. (eds.) AMAST 2004. LNCS, vol.\u00a03116. Springer, Heidelberg (2004)"},{"key":"24_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/978-3-540-37621-7_7","volume-title":"Software Security - Theories and Systems","author":"B. Jacobs","year":"2004","unstructured":"Jacobs, B., Poll, E.: Java Program Verification at Nijmegen: Developments and Perspective. In: Futatsugi, K., Mizoguchi, F., Yonezaki, N. (eds.) ISSS 2003. LNCS, vol.\u00a03233, pp. 134\u2013153. Springer, Heidelberg (2004)"},{"key":"24_CR15","unstructured":"JML home page, http:\/\/www.jmlspecs.org\/"},{"key":"24_CR16","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":"24_CR17","unstructured":"Kiniry, J.: Recent advances in extended static checking. Technical report, KeY Symposium 2007 (2007), http:\/\/www.key-project.org\/keysymposium07\/slides\/kiniry-esc.pdf"},{"key":"24_CR18","unstructured":"KIV homepage, http:\/\/www.informatik.uni-augsburg.de\/swt\/kiv"},{"issue":"3","key":"24_CR19","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1127878.1127884","volume":"31","author":"G.T. Leavens","year":"2006","unstructured":"Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of JML: A behavioral interface specification language for Java. ACM SIGSOFT Software Engineering Notes\u00a031(3), 1\u201338 (2006)","journal-title":"ACM SIGSOFT Software Engineering Notes"},{"key":"24_CR20","unstructured":"Leavens, G.T., Kiniry, J., Poll, E.: A JML tutorial. Technical report, CAV 2007 Tutorial (2007), http:\/\/cav2007.org\/Docs\/Leavens.JML.ps4.pdf"},{"key":"24_CR21","doi-asserted-by":"crossref","unstructured":"March\u00e9, 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(1-2) (2004)","DOI":"10.1016\/j.jlap.2003.07.006"},{"key":"24_CR22","unstructured":"MasterCard International Inc. Mondex, http:\/\/www.mondex.com"},{"key":"24_CR23","volume-title":"Software Engineering and Formal Methods, SEFM","author":"P.H. Schmitt","year":"2007","unstructured":"Schmitt, P.H., Tonin, I.: Verifying the Mondex case study. In: Software Engineering and Formal Methods, SEFM. IEEE Press, Los Alamitos (2007)"},{"key":"24_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"491","DOI":"10.1007\/978-3-540-27815-3_37","volume-title":"Algebraic Methodology and Software Technology","author":"K. Stenzel","year":"2004","unstructured":"Stenzel, K.: A formally verified calculus for full Java Card. In: Rattray, C., Maharaj, S., Shankland, C. (eds.) AMAST 2004. LNCS, vol.\u00a03116, pp. 491\u2013505. Springer, Heidelberg (2004)"},{"key":"24_CR25","unstructured":"Stenzel, K.: Verification of Java Card Programs. PhD thesis, Universit\u00e4t Augsburg, Fakult\u00e4t f\u00fcr Angewandte Informatik (2005)"},{"key":"24_CR26","unstructured":"Sun Microsystems Inc. Java Card 2.2 Specification (2002), http:\/\/java.sun.com\/products\/javacard\/"},{"key":"24_CR27","unstructured":"Ulbrich, M.: Software verification for Java 5. Diplomarbeit, Fakult\u00e4t f\u00fcr Informatik, Universit\u00e4t Karlsruhe (in English, 2007)"}],"container-title":["Lecture Notes in Computer Science","Algebraic Methodology and Software Technology"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-79980-1_24.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T11:35:24Z","timestamp":1619523324000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-79980-1_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540799795","9783540799801"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-79980-1_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}