{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,8]],"date-time":"2025-09-08T06:03:25Z","timestamp":1757311405975,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540408284"},{"type":"electronic","value":"9783540452362"}],"license":[{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/978-3-540-45236-2_24","type":"book-chapter","created":{"date-parts":[[2010,6,25]],"date-time":"2010-06-25T20:08:38Z","timestamp":1277496518000},"page":"422-439","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":55,"title":["Java Applet Correctness: A Developer-Oriented Approach"],"prefix":"10.1007","author":[{"given":"Lilian","family":"Burdy","sequence":"first","affiliation":[]},{"given":"Antoine","family":"Requet","sequence":"additional","affiliation":[]},{"given":"Jean-Louis","family":"Lanet","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,9,25]]},"reference":[{"key":"24_CR1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162","volume-title":"The B Book, Assigning Programs to Meanings","author":"J.-R. Abrial","year":"1996","unstructured":"Abrial, J.-R.: The B Book, Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)"},{"unstructured":"Burdy, L., Requet, A.: Jack: Java Applet Correctness Kit. In: GDC 2002, Singapore (November 2002)","key":"24_CR2"},{"key":"24_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"290","DOI":"10.1007\/3-540-45614-7_17","volume-title":"FME 2002: Formal Methods - Getting IT Right","author":"L. Casset","year":"2002","unstructured":"Casset, L.: Development of an embedded verifier for Java Card byte code using formal methods. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol.\u00a02391, pp. 290\u2013309. Springer, Heidelberg (2002)"},{"doi-asserted-by":"crossref","unstructured":"Casset, L., Burdy, L., Requet, A.: Formal development of an embedded verifier for Java Card byte code. In: DSN 2002, International Conference on Dependable Systems & Networks, Washington, D.C., USA, June 2002, pp. 51\u201356 (2002)","key":"24_CR4","DOI":"10.1007\/3-540-45614-7_17"},{"key":"24_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1007\/3-540-45614-7_16","volume-title":"FME 2002: Formal Methods - Getting IT Right","author":"N. Cata\u00f1o","year":"2002","unstructured":"Cata\u00f1o, N., Huisman, M.: Formal specification and static checking of Gemplus\u2019 electronic purse using ESC\/Java. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol.\u00a02391, pp. 272\u2013289. Springer, Heidelberg (2002)"},{"unstructured":"Cheon, Y., Leavens, G.T.: A runtime assertion checker for the Java Modeling Language (JML). Technical Report 02\u201305, Department of Computer Science, Iowa State University. In SERP 2002, pp. 322\u2013328 (March 2002)","key":"24_CR6"},{"key":"24_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1007\/3-540-47993-7_10","volume-title":"ECOOP 2002 - Object-Oriented Programming","author":"Y. Cheon","year":"2002","unstructured":"Cheon, Y., Leavens, G.T.: A simple and practical approach to unit testing: The JML and JUnit way. In: Magnusson, B. (ed.) ECOOP 2002. LNCS, vol.\u00a02374, pp. 231\u2013255. Springer, Heidelberg (2002)"},{"unstructured":"Filli\u00e2tre, J.-C., March\u00e9, C., Paulin, C., Urbain, X.: Modeling of Java programs in Coq. In: VeriSafe Workshop (September 2002)","key":"24_CR8"},{"key":"24_CR9","series-title":"ACM SIGPLAN Notices","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1145\/512529.512558","volume-title":"Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation (PLDI-02)","author":"C. Flanagan","year":"2002","unstructured":"Flanagan, C., Rustan, K., Leino, M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for java. In: Norris, C., Fenwick Jr., J.B. (eds.) Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation (PLDI-02), June 17\u201319. ACM SIGPLAN Notices, vol.\u00a037, 5, pp. 234\u2013245. ACM Press, New York (2002)"},{"key":"24_CR10","volume-title":"The Java Language Specification","author":"J. Gosling","year":"1996","unstructured":"Gosling, J., Joy, B., Steele, G.: The Java Language Specification. Addison-Wesley, Reading (1996)"},{"unstructured":"Huisman, M.: Java Program Verification in Higher-Order Logic with PVS and Isabelle. PhD thesis, University of Nijmegen, The Netherlands (2001)","key":"24_CR11"},{"key":"24_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1007\/3-540-46428-X_20","volume-title":"Fundamental Approaches to Software Engineering","author":"M. Huisman","year":"2000","unstructured":"Huisman, M., Jacobs, B.: Java program verification via a Hoare logic with abrupt termination. In: Maibaum, T. (ed.) FASE 2000. LNCS, vol.\u00a01783, pp. 284\u2013303. Springer, Heidelberg (2000)"},{"unstructured":"Huisman, M., Jacobs, B., van den Berg, J.: A case study in class library verification: Java\u2019s vector class. CSI Report CSI-R0007, Computing Science Department, Nijmegen (March 2000), \n\nhttp:\/\/www.cs.kun.nl\/csi\/\/reports\/full\/CSI-R0007.ps.Z","key":"24_CR13"},{"key":"24_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1007\/3-540-45314-8_21","volume-title":"Fundamental Approaches to Software Engineering","author":"B. Jacobs","year":"2001","unstructured":"Jacobs, B., Poll, E.: A logic for the Java modeling language JML. In: Hussmann, H. (ed.) FASE 2001. LNCS, vol.\u00a02029, pp. 284\u2013299. Springer, Heidelberg (2001)"},{"unstructured":"Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of JML: A behavioral interface specification language for Java. Technical Report 98\u201306i, Iowa State University, Department of Computer Science (February 2000), \n\nftp:\/\/ftp.cs.iastate.edu\/pub\/techreports\/TR98-06\/TR.ps.gz","key":"24_CR15"},{"key":"24_CR16","first-page":"105","volume-title":"OOPSLA 2000 Companion","author":"G.T. Leavens","year":"2000","unstructured":"Leavens, G.T., Rustan, K., Leino, M., Poll, E., Ruby, C., Jacobs, B.: JML: notations and tools supporting detailed design in Java. In: OOPSLA 2000 Companion, Minneapolis, Minnesota, October 2000, pp. 105\u2013106. ACM Press, New York (2000)"},{"key":"24_CR17","series-title":"Lecture Notes in Computer Science","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","author":"J. Meyer","year":"2000","unstructured":"Meyer, J., Poetzsch-Heffter, A.: An architecture for interactive program provers. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol.\u00a01785, pp. 63\u201377. Springer, Heidelberg (2000)"},{"key":"24_CR18","volume-title":"Fourth Smart Card Research and Advanced Application Conference (IFIP Cardis)","author":"E. Poll","year":"2000","unstructured":"Poll, E., van den Berg, J., Jacobs, B.: Specification of the JavaCard API in JML. In: Fourth Smart Card Research and Advanced Application Conference (IFIP Cardis). Kluwer Academic Publishers, Dordrecht (2000)"},{"key":"24_CR19","series-title":"Lecture Notes in Computer Science","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","author":"J. Berg van den","year":"2001","unstructured":"van den Berg, J., Jacobs, B.: The LOOP compiler for Java and JML. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, pp. 299\u2013312. Springer, Heidelberg (2001)"}],"container-title":["Lecture Notes in Computer Science","FME 2003: Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-45236-2_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,1,23]],"date-time":"2020-01-23T13:09:37Z","timestamp":1579784977000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-45236-2_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540408284","9783540452362"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-45236-2_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]},"assertion":[{"value":"25 September 2003","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}