{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:49:58Z","timestamp":1725486598058},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540729198"},{"type":"electronic","value":"9783540729525"}],"license":[{"start":{"date-parts":[[2007,1,1]],"date-time":"2007-01-01T00:00:00Z","timestamp":1167609600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2007]]},"DOI":"10.1007\/978-3-540-72952-5_14","type":"book-chapter","created":{"date-parts":[[2007,6,26]],"date-time":"2007-06-26T04:10:08Z","timestamp":1182831008000},"page":"221-235","source":"Crossref","is-referenced-by-count":9,"title":["A Refinement Method for Java Programs"],"prefix":"10.1007","author":[{"given":"Holger","family":"Grandy","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kurt","family":"Stenzel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wolfgang","family":"Reif","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"14_CR1","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.S.E. (ed.) ETAPS 2000 and FASE 2000. LNCS, vol.\u00a01783, Springer, Heidelberg (2000)"},{"key":"14_CR2","unstructured":"Tickets on your Mobile. [last seen 2007-03-16] URL: http:\/\/www.beep.nl"},{"key":"14_CR3","first-page":"273","volume-title":"IFM 1999","author":"C. Bolton","year":"1999","unstructured":"Bolton, C., Davies, J., Woodcock, J.C.P.: On the refinement and simulation of data types and processes. In: Araki, K., Galloway, A., Taguchi, K. (eds.) IFM 1999. Proceedings of the International conference of Integrated Formal Methods, pp. 273\u2013292. Springer, Heidelberg (1999)"},{"key":"14_CR4","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-18216-7","volume-title":"Abstract State Machines\u2014A Method for High-Level System Design and Analysis","author":"E. B\u00f6rger","year":"2003","unstructured":"B\u00f6rger, E., St\u00e4rk, R.F.: Abstract State Machines\u2014A Method for High-Level System Design and Analysis. Springer, Heidelberg (2003)"},{"key":"14_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45719-4_21","volume-title":"Algebraic Methodology and Software Technology","author":"C. Breunesse","year":"2002","unstructured":"Breunesse, C., Jacobs, B., van den Berg, J.: Specifying and verifying a decimal representation in Java for smart cards. In: Kirchner, H., Ringeissen, C. (eds.) AMAST 2002. LNCS, vol.\u00a02422, Springer, Heidelberg (2002)"},{"key":"14_CR6","series-title":"Electronic Notes in Theoretical Computer Science","volume-title":"FMICS \u201903","author":"L. Burdy","year":"2003","unstructured":"Burdy, L., Cheon, Y., Cok, D., Ernst, M., Kiniry, J., Leavens, G.T., Rustan, K., Leino, M., Poll, E.: An overview of jml tools and applications. In: Burdy, L., Arts, T., Fokkink, W. (eds.) FMICS \u201903. Eighth International Workshop on Formal Methods for Industrial Critical Systems. Electronic Notes in Theoretical Computer Science, vol.\u00a080, Elsevier, Amsterdam (2003)"},{"key":"14_CR7","doi-asserted-by":"crossref","unstructured":"Burrows, M., Abadi, M., Needham, R.M.: A Logic of Authentication. Technical report, SRC Research Report, 39 (1989)","DOI":"10.1145\/74850.74852"},{"key":"14_CR8","series-title":"Cambridge Tracts in Theoretical Computer Science","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511663079","volume-title":"Data Refinement: Model-Oriented Proof Methods and their Comparison","author":"W. Roever de","year":"1998","unstructured":"de Roever, W., Engelhardt, K.: Data Refinement: Model-Oriented Proof Methods and their Comparison. Cambridge Tracts in Theoretical Computer Science, vol.\u00a047. Cambridge University Press, Cambridge (1998)"},{"key":"14_CR9","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-0257-1","volume-title":"Refinement in Z and in Object-Z: Foundations and Advanced Applications","author":"J. Derrick","year":"2001","unstructured":"Derrick, J., Boiten, E.: Refinement in Z and in Object-Z: Foundations and Advanced Applications. FACIT. Springer, Heidelberg (2001)"},{"key":"14_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/11766155_9","volume-title":"Emerging Trends in Information and Communication Security","author":"H. Grandy","year":"2006","unstructured":"Grandy, H., Haneberg, D., Reif, W., Stenzel, K.: Developing Provably Secure M-Commerce Applications. In: M\u00fcller, G. (ed.) ETRICS 2006. LNCS, vol.\u00a03995, pp. 115\u2013129. Springer, Heidelberg (2006)"},{"key":"14_CR11","unstructured":"Grandy, H., Moebius, N., Bischof, M., Haneberg, D., Schellhorn, G., Stenzel, K., Reif, W.: The Mondex Case Study: From Specifications to Code. Technical Report 2006-31, University of Augsburg (2006) URL: http:\/\/www.informatik.uni-augsburg.de\/lehrstuehle\/swt\/se\/publications\/"},{"key":"14_CR12","unstructured":"Haneberg, D., Schellhorn, G., Grandy, H., Reif, W.: Verification of Mondex Electronic Purses with KIV: From Transactions to a Security Protocol. Technical Report 2006-32, University of Augsburg (2006) URL: http:\/\/www.informatik.uni-augsburg.de\/lehrstuehle\/swt\/se\/publications\/"},{"key":"14_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/3-540-16442-1_14","volume-title":"ESOP 86","author":"H. Jifeng","year":"1986","unstructured":"Jifeng, H., Hoare, C.A.R., Sanders, J.W.: Data refinement refined. In: Robinet, B., Wilhelm, R. (eds.) ESOP 86. LNCS, vol.\u00a0213, pp. 187\u2013196. Springer, Heidelberg (1986)"},{"key":"14_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-39881-3_19","volume-title":"Security in Pervasive Computing","author":"E. Hubbers","year":"2004","unstructured":"Hubbers, E., Oostdijk, M., Poll, E.: Implementing a Formally Verifiable Security Protocol in Java Card. In: Hutter, D., M\u00fcller, G., Stephan, W., Ullmann, M. (eds.) Security in Pervasive Computing. LNCS, vol.\u00a02802, Springer, Heidelberg (2004)"},{"key":"14_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45442-X_11","volume-title":"Mathematics of Program Construction","author":"M. Huisman","year":"2002","unstructured":"Huisman, M.: Verification of java\u2019s abstractcollection class: a case study. In: Boiten, E.A., M\u00f6ller, B. (eds.) MPC 2002. LNCS, vol.\u00a02386, Springer, Heidelberg (2002)"},{"key":"14_CR16","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., Marche, 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":"14_CR17","volume-title":"The Java (tm) Language Specification","year":"2000","unstructured":"Joy, B., Steele, G., Gosling, J., Bracha, G. (eds.): The Java (tm) Language Specification, 2nd edn. Addison-Wesley, Reading (2000)","edition":"2"},{"key":"14_CR18","unstructured":"KIV homepage, http:\/\/www.informatik.uni-augsburg.de\/swt\/kiv"},{"key":"14_CR19","doi-asserted-by":"crossref","unstructured":"Mantel, H.: Preserving Information Flow Properties under Refinement. In: Proceedings of the IEEE Symposium on Security and Privacy, Oakland, CA (2001)","DOI":"10.1109\/SECPRI.2001.924289"},{"key":"14_CR20","unstructured":"Marlet, R., Le Metayer, D.: Verification of Cryptographic Protocols Implemented in JavaCard. In: e-Smart 2003. Proceedings of the e-Smart conference, Sophia Antipolis (2003)"},{"key":"14_CR21","unstructured":"MasterCard International Inc. Mondex. URL: http:\/\/www.mondex.com"},{"key":"14_CR22","unstructured":"Mostowski, W.: Rigorous development of java card applications. In: Clarke, T., Evans, A., Lano, K. (eds.) Proceedings, Fourth Workshop on Rigorous Object-Oriented Methods, London (2002)"},{"key":"14_CR23","doi-asserted-by":"crossref","unstructured":"Paulson, L.C.: The Inductive Approach to Verifying Cryptographic Protocols. J. Computer Security\u00a06 (1998)","DOI":"10.3233\/JCS-1998-61-205"},{"key":"14_CR24","unstructured":"Schellhorn, G., Grandy, H., Haneberg, D., Moebius, N., Reif, W.: A systematic verification Approach for Mondex Electronic Purses using ASMs. Technical Report 2006-27, Universit\u00e4t Augsburg (2006), http:\/\/www.informatik.uni-augsburg.de\/lehrstuehle\/swt\/se\/publications\/"},{"key":"14_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1007\/11813040_2","volume-title":"FM 2006: Formal Methods","author":"G. Schellhorn","year":"2006","unstructured":"Schellhorn, G., Grandy, H., Haneberg, D., Reif, W.: The Mondex Challenge: Machine Checked Proofs for an Electronic Purse. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol.\u00a04085, pp. 16\u201331. Springer, Heidelberg (2006)"},{"key":"14_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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, Springer, Heidelberg (2004)"},{"key":"14_CR27","unstructured":"Stenzel, K.: Verification of Java Card Programs. PhD thesis, Universit\u00e4t Augsburg, Fakult\u00e4t f\u00fcr Angewandte Informatik (2005), http:\/\/www.opus-bayern.de\/uni-augsburg\/volltexte\/2005\/122\/ , or http:\/\/www.informatik.uni-augsburg.de\/forschung\/dissertations\/"},{"key":"14_CR28","unstructured":"Stepney, S., Cooper, D., Woodcock, J.: An Electronic Purse Specification, Refinement, and Proof. Technical monograph PRG-126, Oxford University Computing Laboratory (July 2000), http:\/\/www-users.cs.york.ac.uk\/~susan\/bib\/ss\/z\/monog.htm"},{"key":"14_CR29","unstructured":"Tobler, B., Hutchison, A.: Generating Network Security Protocol Implementations from Formal Specifications. In: CSES 2004. 2nd International Workshop on Certification and Security in Inter-Organizational E-Services at IFIPWorldComputerCongress, Toulouse, France (2004)"},{"key":"14_CR30","series-title":"Prentice Hall International Series in Computer Science","volume-title":"Using Z: Specification, Proof and Refinement","author":"J.C.P. Woodcock","year":"1996","unstructured":"Woodcock, J.C.P., Davies, J.: Using Z: Specification, Proof and Refinement. Prentice Hall International Series in Computer Science. Prentice-Hall, Englewood Cliffs (1996)"},{"issue":"10","key":"14_CR31","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1109\/MC.2006.340","volume":"39","author":"J. Woodcock","year":"2006","unstructured":"Woodcock, J.: First steps in the verified software grand challenge. IEEE Computer\u00a039(10), 57\u201364 (2006)","journal-title":"IEEE Computer"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Open Object-Based Distributed Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-72952-5_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,29]],"date-time":"2019-04-29T16:20:41Z","timestamp":1556554841000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-72952-5_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007]]},"ISBN":["9783540729198","9783540729525"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-72952-5_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2007]]}}}