{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:22:04Z","timestamp":1725488524883},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540421672"},{"type":"electronic","value":"9783540451655"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45165-x_11","type":"book-chapter","created":{"date-parts":[[2007,8,10]],"date-time":"2007-08-10T10:17:47Z","timestamp":1186741067000},"page":"137-150","source":"Crossref","is-referenced-by-count":9,"title":["Formal Specification and Verification of Java Card\u2019s Application Identifier Class"],"prefix":"10.1007","author":[{"given":"Joachim","family":"van den Berg","sequence":"first","affiliation":[]},{"given":"Bart","family":"Jacobs","sequence":"additional","affiliation":[]},{"given":"Erik","family":"Poll","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,6,18]]},"reference":[{"key":"11_CR1","unstructured":"JavaCard API 2.1. http:\/\/www.java.sun.com\/products\/javacard\/htmldoc\/ ."},{"key":"11_CR2","series-title":"Lect. Notes Comp. 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. Mosses, editors, Recent Trends in Algebraic Development Techniques, number 1827 in Lect. Notes Comp. Sci., pages 1\u201321. Springer, Berlin, 2000."},{"key":"11_CR3","unstructured":"J. van den Berg and B. Jacobs. The LOOP compiler for Java and JML. Techn. Rep. CSI-R0019, Comput. Sci. Inst., Univ. of Nijmegen. To appear at TACAS\u201901., 2000."},{"key":"11_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-48957-6","volume-title":"Proceedings of the Java Card 2000 Workshop","author":"J. Berg van den","year":"1999","unstructured":"J. van den Berg, B. Jacobs, and E. Poll. Formal specification and verification of JavaCard\u2019s Application Identifier Class. Techn. Rep. CSI-R0014, Comput. Sci. Inst., Univ. of Nijmegen. Appeared in: Proceedings of the JavaCard Workshop, Cannes. INRIA Techn. Rep. Updated version will appear in: I. Attali and Th. Jensen, editors, Proceedings of the Java Card 2000 Workshop (Springer LNCS 2001), Sept. 1999."},{"key":"11_CR5","unstructured":"A. Bhorkar. A run-time assertion checker for Java using JML. Techn. Rep. 00-08, Dep. of Comp. Science, Iowa State Univ. ( http:\/\/www.cs.iastate.edu\/~leavens\/JML.html ), 2000."},{"key":"11_CR6","unstructured":"Z. Chen. Java Card Technologyfor Smart Cards. The Java Series. Addison-Wesley, 2000."},{"key":"11_CR7","volume-title":"Technical report","author":"D. Detlefs","year":"1998","unstructured":"D. Detlefs, K. R. M. Leino, and G. Nelson. Wrestling with rep exposure. Technical report, Compaq Systems Research Center, Palo Alto, 1998. Research Report 156."},{"key":"11_CR8","doi-asserted-by":"crossref","unstructured":"M. Huisman, B. Jacobs, and J. van den Berg. A case study in class library verification: Java\u2019s Vector class. Techn. Rep. CSI-R0007, Comput. Sci. Inst., Univ. of Nijmegen. To appear in Software Tools for Technology Transfer, 2001.","DOI":"10.1007\/s100090100047"},{"key":"11_CR9","series-title":"Lect. Notes Comp. Sci","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1007\/3-540-46428-X_15","volume-title":"Fundamental Approaches to Software Engineering","author":"K. Huizing","year":"2000","unstructured":"K. Huizing, R. Kuiper, and SOOP. Verification of object oriented programs using class invariants. In T. Maibaum, editor, Fundamental Approaches to Software Engineering, number 1783 in Lect. Notes Comp. Sci., pages 208\u2013221. Springer, Berlin, 2000."},{"key":"11_CR10","unstructured":"B. Jacobs and E. Poll. A logic for the Java Modeling Language JML. Techn. Rep. CSI-R0018, Comput. Sci. Inst., Univ. of Nijmegen. To appear at FASE\u201901., 2000."},{"key":"11_CR11","doi-asserted-by":"crossref","unstructured":"B. Jacobs, J. van den Berg, M. Huisman, M. van Berkum, U. Hensel, and H. Tews. Reasoning about classes in Java (preliminary report). In Object-Oriented Programming, Systems, Languages and Applications (OOPSLA), pages 329\u2013340. ACM Press, 1998.","DOI":"10.1145\/286942.286973"},{"key":"11_CR12","doi-asserted-by":"crossref","unstructured":"G.T. Leavens, A.L. Baker, and C. Ruby. JML: A notation for detailed design. In H. Kilov and B. Rumpe, editors, Behavioral Specifications of Business and Systems, pages 175\u2013188. Kluwer, 1999.","DOI":"10.1007\/978-1-4615-5229-1_12"},{"key":"11_CR13","unstructured":"G.T. Leavens, A.L. Baker, and C. Ruby. Preliminary design of JML: A behavioral interface specification language for Java. Techn. Rep. 98-06, Dep. of Comp. Sci., Iowa State Univ. ( http:\/\/www.cs.iastate.edu\/~leavens\/JML.html ), 1999."},{"issue":"2","key":"11_CR14","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1109\/32.345827","volume":"21","author":"S. Owre","year":"1995","unstructured":"S. Owre, J.M. Rushby, N. Shankar, and F. von Henke. Formal verification for fault-tolerant architectures: Prolegomena to the design of PVS. IEEE Trans. on Softw. Eng., 21(2):107\u2013125, 1995.","journal-title":"IEEE Trans. on Softw. Eng"},{"key":"11_CR15","series-title":"Lect. Notes Comp. Sci","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/3-540-49099-X_11","volume-title":"Programming Languages and Systems","author":"A. Poetzsch-Heffter","year":"1999","unstructured":"A. Poetzsch-Heffter and P. M\u00fcller. A programming logic for sequential Java. In S.D. Swierstra, editor, Programming Languages and Systems, number 1576 in Lect. Notes Comp. Sci., pages 162\u2013176. Springer, Berlin, 1999."},{"key":"11_CR16","doi-asserted-by":"crossref","unstructured":"E. Poll, J. van den Berg, and B. Jacobs. Specification of the JavaCard API in JML. In J. Domingo-Ferrer, D. Chan, and A. Watson, editors, Smart Card Research and Advanced Application, pages 135\u2013154. Kluwer Acad. Publ., 2000.","DOI":"10.1007\/978-0-387-35528-3_8"},{"key":"11_CR17","doi-asserted-by":"crossref","unstructured":"E. Poll, J. van den Berg, and B. Jacobs. Formal specification of the JavaCard API in JML: the APDU class. Comp. Networks Mag., 2001. To appear.","DOI":"10.1016\/S1389-1286(01)00163-3"},{"key":"11_CR18","unstructured":"Extended static checker ESC\/Java. Compaq System Research Center. http:\/\/www.research.digital.com\/SRC\/esc\/Esc.html ."},{"key":"11_CR19","unstructured":"C. Szyperski. Component Software. Addison-Wesley, 1998."}],"container-title":["Lecture Notes in Computer Science","Java on Smart Cards:Programming and Security"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45165-X_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,25]],"date-time":"2020-04-25T19:33:16Z","timestamp":1587843196000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45165-X_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540421672","9783540451655"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/3-540-45165-x_11","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}