{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T20:30:37Z","timestamp":1761597037553},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540426103"},{"type":"electronic","value":"9783540454182"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45418-7_14","type":"book-chapter","created":{"date-parts":[[2007,6,3]],"date-time":"2007-06-03T17:08:09Z","timestamp":1180890489000},"page":"165-178","source":"Crossref","is-referenced-by-count":14,"title":["Towards a Full Formal Specification of the JavaCard API"],"prefix":"10.1007","author":[{"given":"Hans","family":"Meijer","sequence":"first","affiliation":[]},{"given":"Erik","family":"Poll","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,9,11]]},"reference":[{"key":"14_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/3-540-45319-9_21","volume-title":"Tools ans Algorithms for the Construction and Analysis of Software (TACAS)","author":"J. Berg van den","year":"2001","unstructured":"J. van den Berg and B. Jacobs. The LOOP compiler for Java and JML. In T. Margaria and W. Yi, editors, Tools ans Algorithms for the Construction and Analysis of Software (TACAS), number 2031 in LNCS, pages 299\u2013312. Springer, Berlin, 2001."},{"key":"14_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-44503-X","volume-title":"Proceeding of the first JavaCard Workshop (JCW\u20192000)","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 I. Attali and T. Jensen, editors, Proceeding of the first JavaCard Workshop (JCW\u20192000), LNCS. Springer Verlag, 2001. To appear."},{"key":"14_CR3","series-title":"Lect Notes Comput Sci","volume-title":"10th Formal Methods for Increasing Software Productivity (FME)","author":"P. H. Hartel","year":"2001","unstructured":"P. H. Hartel, M. J. Butler, E. de Jong, and M. Longley. Transacted memory for smart cards. In 10th Formal Methods for Increasing Software Productivity (FME), LNCS. Springer Verlag, 2001."},{"key":"14_CR4","doi-asserted-by":"crossref","unstructured":"P. H. Hartel and L. A. V. Moreau. Formalizing the safety of Java, the Java virtual machine and Java Card. ACM Computing Surveys, 2001. to appear.","DOI":"10.1145\/503112.503115"},{"key":"14_CR5","unstructured":"The Java Card 2.1.1 Application Programming Interface (API). Sun Microsystems, 2000."},{"key":"14_CR6","unstructured":"The Java Card 2.1.1 Runtime Environment (JCRE) Specification. Sun Microsystems, 2000."},{"key":"14_CR7","unstructured":"The Java Card 2.1.1 Virtual Machine (JCVM) Specification. Sun Microsystems, 2000."},{"key":"14_CR8","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":"14_CR9","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. (\n                    http:\/\/www.cs.iastate.edu\/~leavens\/JML.html\n                    \n                  ), 1999."},{"key":"14_CR10","unstructured":"B. Meyer. Object-Oriented Software Construction. Prentice Hall, 2\n                           nd rev. edition, 1997."},{"key":"14_CR11","unstructured":"St\u00e9phanie Motr\u00e9. Formal model and implementation of the Java Card dynamic security policy. Technical Report SM-99-09, Gemplus Research Lab, 1999. Presented at AFADL\u20192000."},{"key":"14_CR12","doi-asserted-by":"crossref","unstructured":"Marcus Oestreicher. Transactions in Java Card. In 15th Annual Computer Security Applications Conference (ACSAC\u201999), pages 291\u2013298. IEEE, 1999.","DOI":"10.1109\/CSAC.1999.816039"},{"key":"14_CR13","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, Fourth Smart Card Research and Advanced Application Conference (CARDIS\u20192000), pages 135\u2013154. Kluwer Acad. Publ., 2000.","DOI":"10.1007\/978-0-387-35528-3_8"},{"key":"14_CR14","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. Computer Networks, 2001. To appear.","DOI":"10.1016\/S1389-1286(01)00163-3"},{"issue":"3","key":"14_CR15","doi-asserted-by":"crossref","first-page":"145","DOI":"10.1023\/A:1026538301096","volume":"17","author":"D. Sabatier","year":"2000","unstructured":"Denis Sabatier and Pierre Lartigue. The use of the B formal method for the design and the validation of the transaction mechanism for smart card applications. Formal Method in System Design, 17(3):145\u2013272, 2000. Special issue on FM\u201999.","journal-title":"Formal Method in System Design"}],"container-title":["Lecture Notes in Computer Science","Smart Card Programming and Security"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45418-7_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,16]],"date-time":"2019-02-16T23:08:49Z","timestamp":1550358529000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45418-7_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540426103","9783540454182"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/3-540-45418-7_14","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}