{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T20:25:10Z","timestamp":1761596710128},"reference-count":18,"publisher":"Elsevier BV","issue":"4","license":[{"start":{"date-parts":[[2001,7,1]],"date-time":"2001-07-01T00:00:00Z","timestamp":993945600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Computer Networks"],"published-print":{"date-parts":[[2001,7]]},"DOI":"10.1016\/s1389-1286(01)00163-3","type":"journal-article","created":{"date-parts":[[2002,7,25]],"date-time":"2002-07-25T20:42:39Z","timestamp":1027629759000},"page":"407-421","source":"Crossref","is-referenced-by-count":22,"title":["Formal specification of the JavaCard API in JML: the APDU class"],"prefix":"10.1016","volume":"36","author":[{"given":"Erik","family":"Poll","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joachim","family":"van den Berg","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bart","family":"Jacobs","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"issue":"4","key":"10.1016\/S1389-1286(01)00163-3_BIB1","doi-asserted-by":"crossref","first-page":"431","DOI":"10.1145\/357146.357150","article-title":"Ten years of Hoare's logic: a survey \u2013 Part I","volume":"3","author":"Apt","year":"1981","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"10.1016\/S1389-1286(01)00163-3_BIB2","doi-asserted-by":"crossref","unstructured":"J. van den Berg, M. Huisman, B. Jacobs, E. Poll, A type-theoretic memory model for verification of sequential Java programs, in: D. Bert, C. Choppy (Eds), Recent Trends in Algebraic Development Techniques (WADT'99), Lecture Notes in Computer Science, vol. 1827, Springer, Berlin, 2000","DOI":"10.1007\/978-3-540-44616-3_1"},{"key":"10.1016\/S1389-1286(01)00163-3_BIB3","unstructured":"J. van den Berg, B. Jacobs, E. Poll, Formal specification and verification of JavaCard's application identifier class, in: I. Attali, T. Jensen (Eds.), JavaCard Workshop (JCW'2000), INRIA, Sophia Antipolis, 2000"},{"key":"10.1016\/S1389-1286(01)00163-3_BIB4","series-title":"Java Card Technology for Smart Cards: Architecture and Programmer's Guide","author":"Chen","year":"2000"},{"key":"10.1016\/S1389-1286(01)00163-3_BIB5","unstructured":"Extended static checker ESC\/Java, Compaq System Reserch Center. http:\/\/www.research.digital.com\/SRC\/esc\/Esc.html"},{"key":"10.1016\/S1389-1286(01)00163-3_BIB6","doi-asserted-by":"crossref","unstructured":"M. Huisman, B. Jacobs, Java program verification via a Hoare logic with abrupt termination, in: T. Maibaum (Ed.), Fundamental Approaches to Software Engineering, Lecture Notes in Computer Science, vol. 1783, Springer, Berlin, 2000, pp. 284\u2013303","DOI":"10.1007\/3-540-46428-X_20"},{"key":"10.1016\/S1389-1286(01)00163-3_BIB7","unstructured":"M. Huisman, B. Jacobs, J. van den Berg, A case study in class library verification: Java's Vector class, Software Tools for Technology Transfer, to appear"},{"key":"10.1016\/S1389-1286(01)00163-3_BIB8","doi-asserted-by":"crossref","unstructured":"B. Jacobs, J. van den Berg, M. Huisman, M. van Berkum, U. Hensel, H. Tews, Reasoning about classes in Java (preliminary report), in: Object-oriented Programming, Systems, Languages and Applications (OOPSLA), ACM Press, New York, 1998, pp. 329\u2013340","DOI":"10.1145\/286942.286973"},{"key":"10.1016\/S1389-1286(01)00163-3_BIB9","unstructured":"The Java Card 2.1.1 Application Programming Interface (API), Sun Microsystems, 2000"},{"key":"10.1016\/S1389-1286(01)00163-3_BIB10","doi-asserted-by":"crossref","unstructured":"G.T. Leavens, A.L. Baker, C. Ruby, JML: A notation for detailed design, in: H. Kilov, B. Rumpe, I. Simmonds (Eds.), Behavioral Specifications of Businesses and Systems, Kluwer Academic Publishers, Dordrecht, 1999, pp. 175\u2013188","DOI":"10.1007\/978-1-4615-5229-1_12"},{"key":"10.1016\/S1389-1286(01)00163-3_BIB11","unstructured":"G.T. Leavens, A.L. Baker, C. Ruby, Preliminary design of JML: a behavioral interface specification language for Java, Tech. Rep. 98-06, Dept. Comp. Sci., Iowa State University, 1999"},{"key":"10.1016\/S1389-1286(01)00163-3_BIB12","doi-asserted-by":"crossref","unstructured":"G.T. Leavens, K.R.M. Leino, E. Poll, C. Ruby, B. Jacobs, JML: notations and tools supporting detailed design in Java, in: OOPSLA'2000 Companion, ACM, 2000; Tech. Rep. TR00-15, Dept. Computer Science, Iowa State University, August 2000","DOI":"10.1145\/367845.367996"},{"key":"10.1016\/S1389-1286(01)00163-3_BIB13","unstructured":"K.R.M. Leino, J.B. Saxe, R. Stata, Checking Java programs via guarded commands, in: B. Jacobs, G.T. Leavens, P.M\u00fcller, A. Poetzsch-Heffter (Eds.), Formal Techniques for Java Programs, Proceedings of the ECOOP'99 Workshop, pp. 37\u201344; Tech. Rep. 251, Fernuniversit\u00e4t Hagen, 1999; Tech. Note 1999-002, Compaq Systems Research Center, Palo Alto"},{"key":"10.1016\/S1389-1286(01)00163-3_BIB14","unstructured":"The LOOP project. http:\/\/www.cs.kun.nl\/\u223cbart\/LOOP\/index.html"},{"key":"10.1016\/S1389-1286(01)00163-3_BIB15","series-title":"Object-oriented Software Construction","author":"Meyer","year":"1997"},{"key":"10.1016\/S1389-1286(01)00163-3_BIB16","doi-asserted-by":"crossref","unstructured":"S. Owre, S. Rajan, J.M. Rushby, N. Shankar, M. Srivas, PVS: combining specification, proof checking, and model checking, in: R. Alur, T.A. Henzinger (Eds.), Computer Aided Verification, Lecture Notes in Computer Science, vol. 1102, Springer, Berlin, 1996, pp. 411\u2013414","DOI":"10.1007\/3-540-61474-5_91"},{"key":"10.1016\/S1389-1286(01)00163-3_BIB17","doi-asserted-by":"crossref","unstructured":"L.C. Paulson, Isabelle: A Generic Theorem Prover, Lecture Notes in Computer Science, vol. 828, Springer, Germany, 1994","DOI":"10.1007\/BFb0030541"},{"key":"10.1016\/S1389-1286(01)00163-3_BIB18","doi-asserted-by":"crossref","unstructured":"E. Poll, J. van den Berg, B. Jacobs, Specification of the JavaCard API in JML, in: J. Domingo-Ferrer, D. Chan, A. Watson (Eds.), Fourth Smart Card Research and Advanced Application Conference (CARDIS'2000), Kluwer Academic Publishers, Dordrecht, 2000, pp. 135\u2013154","DOI":"10.1007\/978-0-387-35528-3_8"}],"container-title":["Computer Networks"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1389128601001633?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1389128601001633?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,2,4]],"date-time":"2020-02-04T13:50:29Z","timestamp":1580824229000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1389128601001633"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001,7]]},"references-count":18,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2001,7]]}},"alternative-id":["S1389128601001633"],"URL":"https:\/\/doi.org\/10.1016\/s1389-1286(01)00163-3","relation":{},"ISSN":["1389-1286"],"issn-type":[{"value":"1389-1286","type":"print"}],"subject":[],"published":{"date-parts":[[2001,7]]}}}