{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,9]],"date-time":"2026-05-09T03:51:24Z","timestamp":1778298684242,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540439288","type":"print"},{"value":"9783540456148","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45614-7_16","type":"book-chapter","created":{"date-parts":[[2007,5,17]],"date-time":"2007-05-17T04:45:28Z","timestamp":1179377128000},"page":"272-289","source":"Crossref","is-referenced-by-count":21,"title":["Formal Specification and Static Checking of Gemplus\u2019 Electronic Purse Using ESC\/Java"],"prefix":"10.1007","author":[{"given":"N\u00e9stor","family":"Cata\u00f1o","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marieke","family":"Huisman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,7,9]]},"reference":[{"key":"16_CR1","unstructured":"E. Bretagne, A. El Marouani, P. Girard, and J.-L. Lanet. Pacap purse and loyalty specification. Technical Report V 0.4, Gemplus, 2000."},{"key":"16_CR2","series-title":"Lect Notes Comput Sci","volume-title":"Algebraic Methodology And Software Technology (AMAST\u2019 02)","author":"C. Breunesse","year":"2002","unstructured":"C. Breunesse, B. Jacobs, and J. van den Berg. Specifying and Verifying a Decimal Representation in Java for Smart Cards. In Algebraic Methodology And Software Technology (AMAST\u2019 02), LNCS. Springer, 2002. To appear."},{"key":"16_CR3","unstructured":"N. Cata\u00f1o and M. Huisman. Annotated files Electronic Purse case study, 2001. http:\/\/www-sop.inria.fr\/lemme\/verificard\/electronicpurse ."},{"key":"16_CR4","doi-asserted-by":"crossref","unstructured":"N. Cata\u00f1o and M. Huisman. A static checker for JML\u2019s assignable clause, 2002. Manuscript.","DOI":"10.1007\/3-540-36384-X_6"},{"key":"16_CR5","unstructured":"Differences between Esc\/Java and JML, 2000. Comes with JML distribution, in file esc-jml-diffs.txt."},{"key":"16_CR6","unstructured":"Extended static checking for Java. http:\/\/research.compaq.com\/SRC\/esc\/ ."},{"key":"16_CR7","unstructured":"ESC\/Java specifications for the JavaCard API. http:\/\/www.cs.kun.nl\/~erikpoll\/publications\/jc211specs.html ."},{"key":"16_CR8","unstructured":"Gemplus. Applet benchmark kit. http:\/\/www.gemplus.com\/smart\/rd\/publications\/case-study\/ ."},{"key":"16_CR9","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":"16_CR10","unstructured":"The JASS project. http:\/\/semantik.informatik.uni-oldenburg.de\/~jass\/ ."},{"key":"16_CR11","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, 2000."},{"key":"16_CR12","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."},{"key":"16_CR13","unstructured":"The LOOP project. http:\/\/www.cs.kun.nl\/~bart\/LOOP\/ ."},{"key":"16_CR14","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1007\/3-540-45418-7_14","volume-title":"Smart Card Programming and Security (E-smart 2001)","author":"H. Meijer","year":"2001","unstructured":"H. Meijer and E. Poll. Towards a Full Formal Specification of the Java Card API. In I. Attali and T. Jensen, editors, Smart Card Programming and Security (E-smart 2001), number 2140 in LNCS, pages 165\u2013178. Springer, 2001."},{"key":"16_CR15","unstructured":"B. Meyer. Object-Oriented Software Construction. Prentice Hall, 2nd rev. edition, 1997."},{"key":"16_CR16","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1007\/3-540-46419-0_6","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2000)","author":"J. Meyer","year":"2000","unstructured":"J. Meyer and A. Poetzsch-Heffter. An architecture of interactive program provers. In S. Graf and M. Schwartzbach, editors, Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2000), number 1785 in LNCS, pages 63\u201377. Springer, 2000."},{"key":"16_CR17","unstructured":"Sun Microsystems, Inc. Java Card 2.1. Platform Application Programming Interface (API) Specification. http:\/\/java.sun.com\/products\/javacard\/htmldoc\/ ."},{"key":"16_CR18","unstructured":"Sun Microsystems, Inc. JavaCard Technology. http:\/\/java.sun.com\/products\/javacard\/ ."},{"key":"16_CR19","series-title":"Lect Notes Comput Sci","volume-title":"Algebraic Methodology And Software Technology (AMAST\u2019 02)","author":"K. Trentelman","year":"2002","unstructured":"K. Trentelman and M. Huisman. Extending JML Specifications with Temporal Logic. In Algebraic Methodology And Software Technology (AMAST\u2019 02), LNCS. Springer, 2002. To appear."}],"container-title":["Lecture Notes in Computer Science","FME 2002:Formal Methods\u2014Getting IT Right"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45614-7_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,22]],"date-time":"2020-04-22T04:12:30Z","timestamp":1587528750000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45614-7_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439288","9783540456148"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/3-540-45614-7_16","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2002]]}}}