{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:05:39Z","timestamp":1725483939691},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540438571"},{"type":"electronic","value":"9783540454427"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45442-x_11","type":"book-chapter","created":{"date-parts":[[2007,5,15]],"date-time":"2007-05-15T04:55:08Z","timestamp":1179204908000},"page":"175-194","source":"Crossref","is-referenced-by-count":7,"title":["Verification of Java\u2019s AbstractCollection Class: A Case Study"],"prefix":"10.1007","author":[{"given":"Marieke","family":"Huisman","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,6,21]]},"reference":[{"key":"11_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1007\/BFb0019440","volume-title":"Foundations of Object-Oriented Languages","author":"P. America","year":"1990","unstructured":"P. America. Designing an object-oriented programming language with behavioural subtyping. In J.W. de Bakker, W.P. de Roever, and G. Rozenberg, editors, Foundations of Object-Oriented Languages, number 489 in LNCS, pages 60\u201390. Springer, 1990."},{"key":"11_CR2","unstructured":"K. Arnold, J. Gosling, and D. Holmes. The Java Programming Language. Addison-Wesley, 3nd edition, 2000."},{"key":"11_CR3","series-title":"Lect Notes Comput Sci","first-page":"1","volume-title":"Recent Trends in Algebraic Development Techniques","author":"J. Berg van den","year":"2000","unstructured":"J. van den Berg, M. Huisman, B. Jacobs, and E. Poll. A type-theoretic memory model for verification of sequential Java programs. In D. Bert, C. Choppy, and P.D. Mosses, editors, Recent Trends in Algebraic Development Techniques, number 1827 in LNCS, pages 1\u201321. Springer, 2000."},{"key":"11_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/3-540-45319-9_21","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2001)","author":"J. Berg van den","year":"2001","unstructured":"J. van den Berg and B. Jacobs. The LOOP compiler for Java and JML. In T. Mar-garia and W. Yi, editors, Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2001), number 2031 in LNCS, pages 299\u2013312. Springer, 2001."},{"key":"11_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1007\/3-540-45165-X_11","volume-title":"Java on Smart Cards: Programming and Security","author":"J. Berg van den","year":"2001","unstructured":"J. van den Berg, B. Jacobs, and E. Poll. Formal Specification and Verification of JavaCard\u2019s Application Identifier Class. In Java on Smart Cards: Programming and Security, number 2041 in LNCS, pages 137\u2013150. Springer, 2001."},{"key":"11_CR6","doi-asserted-by":"crossref","unstructured":"C. Breunesse, B. Jacobs, and J. van den Berg. Specifying and Verifying an Example: a decimal representation in Java for smartcards, 2002. Manuscript.","DOI":"10.1007\/3-540-45719-4_21"},{"key":"11_CR7","unstructured":"T. Budd. Understanding Object-oriented programming with Java-updated edition. Addison-Wesley, 2000."},{"key":"11_CR8","series-title":"Lect Notes Comput Sci","volume-title":"Formal Methods Europe (FME\u201902)","author":"N. Cata\u00f1o","year":"2002","unstructured":"N. Cata\u00f1o and M. Huisman. Formal specification of Gemplus\u2019 electronic purse case study. In Formal Methods Europe (FME\u201902), LNCS. Springer, 2002. To appear."},{"key":"11_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"389","DOI":"10.1007\/BFb0053388","volume-title":"European Conference on Object-Oriented Programming","author":"S. Drossopoulou","year":"1997","unstructured":"S. Drossopoulou and S. Eisenbach. Java is type safe-probably. In M. Aksit, editor, European Conference on Object-Oriented Programming, number 1241 in LNCS, pages 389\u2013418. Springer, 1997."},{"key":"11_CR10","unstructured":"ESC\/Java specifications for the JavaCard API. http:\/\/www.cs.kun.nl\/~erikpoll\/publications\/jc211_specs.html ."},{"issue":"5","key":"11_CR11","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1109\/MS.1985.231756","volume":"2","author":"J. Guttag","year":"1985","unstructured":"J. Guttag, J. Horning, and J. Wing. The Larch family of specification languages. IEEE Software, 2(5):24\u201336, 1985.","journal-title":"IEEE Software"},{"key":"11_CR12","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/BF00289507","volume":"1","author":"C.A.R. Hoare","year":"1972","unstructured":"C.A.R. Hoare. Proof of correctness of data representations. Acta Informatica, 1:271\u2013281, 1972.","journal-title":"Acta Informatica"},{"key":"11_CR13","unstructured":"M. Huisman. Specifications of Java\u2019s Collection class. http:\/\/www-sop.inria.fr\/lemme\/Marieke.Huisman\/collection.html ."},{"key":"11_CR14","unstructured":"M. Huisman. Reasoning about Java programs in higher order logic using PVS and Isabelle. PhD thesis, Computing Science Institute, University of Nijmegen, 2001."},{"key":"11_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1007\/3-540-46428-X_20","volume-title":"Fundamental Approaches to Software Engineering (FASE 2000)","author":"M. Huisman","year":"2000","unstructured":"M. Huisman and B. Jacobs. Java program verification via a Hoare logic with abrupt termination. In T. Maibaum, editor, Fundamental Approaches to Software Engineering (FASE 2000), number 1783 in LNCS, pages 284\u2013303. Springer, 2000."},{"key":"11_CR16","doi-asserted-by":"crossref","first-page":"332","DOI":"10.1007\/s100090100047","volume":"3\/3","author":"M. Huisman","year":"2001","unstructured":"M. Huisman, B. Jacobs, and J. van den Berg. A Case Study in Class Library Verification: Java\u2019s Vector Class. Software Tools for Technology Transfer, 3\/3:332\u2013352, 2001.","journal-title":"Software Tools for Technology Transfer"},{"key":"11_CR17","unstructured":"K. Huizing and R. Kuiper. Reinforcing fragile base classes. In Proceedings of Workshop on Formal Techniques for Java Programs (FTfJP), 2001."},{"key":"11_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1007\/3-540-45314-8_21","volume-title":"Fundamental Approaches to Software Engineering (FASE 2001)","author":"B. Jacobs","year":"2001","unstructured":"B. Jacobs and E. Poll. A logic for the Java Modeling Language JML. In H. Hussmann, editor, Fundamental Approaches to Software Engineering (FASE 2001), number 2029 in LNCS, pages 284\u2013299. Springer, 2001."},{"key":"11_CR19","unstructured":"Java\u2122 2 platform, standard edition, version 1.3 API specification. http:\/\/www.java.sun.com\/j2se\/1.3\/docs\/api\/index.html ."},{"key":"11_CR20","unstructured":"G.T. Leavens, A.L. Baker, and C. Ruby. Preliminary design of JML: A behavioral interface specification language for Java. Technical Report 98-06, Iowa State University, Department of Computer Science, 1998."},{"key":"11_CR21","unstructured":"K.R.M. Leino. Toward Reliable Modular Programs. PhD thesis, California Inst. of Techn., 1995."},{"key":"11_CR22","unstructured":"K.R.M. Leino, G. Nelson, and J. B. Saxe. ESC\/Java User\u2019s Manual. Technical Report SRC 2000-002, Compaq System Research Center, 2000."},{"issue":"1","key":"11_CR23","doi-asserted-by":"publisher","first-page":"1811","DOI":"10.1145\/197320.197383","volume":"16","author":"B.H. Liskov","year":"1994","unstructured":"B.H. Liskov and J.M. Wing. A behavioral notion of subtyping. ACM Trans. on Progr. Lang. and Systems, 16(1):1811\u20131841, 1994.","journal-title":"ACM Trans. on Progr. Lang. and Systems"},{"key":"11_CR24","unstructured":"The LOOP project. http:\/\/www.cs.kun.nl\/~bart\/LOOP\/index.html ."},{"key":"11_CR25","unstructured":"B. Meyer. Object-Oriented Software Construction. Prentice Hall, 2nd rev. edition, 1997."},{"key":"11_CR26","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1007\/3-540-48737-9_4","volume-title":"Formal Syntax and Semantics of Java","author":"D. Oheimb von","year":"1999","unstructured":"D. von Oheimb and T. Nipkow. Machine-checking the Java specification: Proving type-safety. In J. Alves-Foss, editor, Formal Syntax and Semantics of Java, number 1523 in LNCS, pages 119\u2013156. Springer, 1999."},{"issue":"2","key":"11_CR27","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1109\/32.345827","volume":"21","author":"S. Owre","year":"1995","unstructured":"S. Owre, J. Rushby, N. Shankar, and F von Henke. Formal verification for fault-tolerant architectures: Prolegomena to the design of PVS. IEEE Transactions on Software Engineering, 21(2):107\u2013125, 1995.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"11_CR28","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle-a generic theorem prover","author":"L.C. Paulson","year":"1994","unstructured":"L.C. Paulson. Isabelle-a generic theorem prover. Number 828 in LNCS. Springer, 1994. With contributions by Tobias Nipkow."},{"key":"11_CR29","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/3-540-48737-9_3","volume-title":"Formal Syntax and Semantics of Java","author":"D. Syme","year":"1999","unstructured":"D. Syme. Proving Java type soundness. In J. Alves-Foss, editor, Formal Syntax and Semantics of Java, number 1523 in LNCS, pages 83\u2013118. Springer, 1999."}],"container-title":["Lecture Notes in Computer Science","Mathematics of Program Construction"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45442-X_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,22]],"date-time":"2020-04-22T00:54:00Z","timestamp":1587516840000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45442-X_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540438571","9783540454427"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/3-540-45442-x_11","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}