{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,1]],"date-time":"2026-04-01T14:19:54Z","timestamp":1775053194110,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540242871","type":"print"},{"value":"9783540305699","type":"electronic"}],"license":[{"start":{"date-parts":[[2005,1,1]],"date-time":"2005-01-01T00:00:00Z","timestamp":1104537600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/978-3-540-30569-9_6","type":"book-chapter","created":{"date-parts":[[2010,7,4]],"date-time":"2010-07-04T17:59:08Z","timestamp":1278266348000},"page":"108-128","source":"Crossref","is-referenced-by-count":109,"title":["ESC\/Java2: Uniting ESC\/Java and JML"],"prefix":"10.1007","author":[{"given":"David R.","family":"Cok","sequence":"first","affiliation":[]},{"given":"Joseph R.","family":"Kiniry","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"6_CR1","unstructured":"Many references to papers on JML can be found on the JML project website, http:\/\/www.cs.iastate.edu\/~leavens\/JML\/papers.shtml"},{"key":"6_CR2","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.v.d. Berg","year":"2001","unstructured":"Berg, J.v.d., 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)"},{"key":"6_CR3","series-title":"Electronic Notes in Theoretical Computer Science (ENTCS)","first-page":"73","volume-title":"Eighth International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2003)","author":"L. Burdy","year":"2003","unstructured":"Burdy, L., Cheon, Y., Cok, D.R., Ernst, M., Kiniry, J., Leavens, G.T., Leino, K.R.M., Poll, E.: An overview of JML tools and applications. In: Arts, T., Fokkink, W. (eds.) Eighth International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2003). Electronic Notes in Theoretical Computer Science (ENTCS), vol.\u00a080, pp. 73\u201389. Elsevier, Amsterdam (2003)"},{"key":"6_CR4","unstructured":"Burdy, L., Requet, A.: JACK: Java applet correctness kit. In: Proceedings, 4th Gemplus Developer Conference, Singapore (November 2002)"},{"key":"6_CR5","doi-asserted-by":"crossref","unstructured":"Breunesse, J.v.C.-B., Jacobs, B.: Specifying and verifying a decimal representation in Java for smart cards. In: Kirchner, H., Ringeissen, C. (eds.) AMAST 2002. LNCS, vol.\u00a02422, pp. 304\u2013318. Springer, Heidelberg (2002)","DOI":"10.1007\/3-540-45719-4_21"},{"key":"6_CR6","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 of Gemplus\u2019 electronic purse case study using ESC\/Java. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol.\u00a02391, pp. 272\u2013289. Springer, Heidelberg (2002)"},{"key":"6_CR7","doi-asserted-by":"crossref","unstructured":"Chalin, P.: JML support for primitive arbitrary precision numeric types: Definition and semantics. In: Proceedings, ECOOP 2003 Workshop on Formal Techniques for Java-like Programs (FTfJP), Darmstadt, Germany (July 2003)","DOI":"10.5381\/jot.2004.3.6.a3"},{"key":"6_CR8","unstructured":"Cheon, Y., Leavens, G.T., Sitaraman, M., Edwards, S.: Model variables: Cleanly supporting abstraction in design by contract. Technical Report 03-10a, Department of Computer Science, Iowa State University (September 2003), Available from http:\/\/archives.cs.iastate.edu\/"},{"key":"6_CR9","doi-asserted-by":"crossref","unstructured":"Clarke, E., Wing, J.: Strategic directions in computing research: Tools and partial analysis. ACM Computing Surveys\u00a028A(4) (December 1996)","DOI":"10.1145\/242224.242374"},{"key":"6_CR10","unstructured":"Cok, D.R.: Esc\/java2 implementation notes. Included with all ESC\/Java2 releases (2004)"},{"key":"6_CR11","doi-asserted-by":"crossref","unstructured":"Csallner, C., Smaragdakis, Y.: Check \u2019n Crash: Combining static checking and testing. Submitted for publication (2005)","DOI":"10.1145\/1062455.1062533"},{"key":"6_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"500","DOI":"10.1007\/3-540-45251-6_29","volume-title":"FME 2001: Formal Methods for Increasing Software Productivity","author":"C. Flanagan","year":"2001","unstructured":"Flanagan, C., Leino, K.R.M.: Houdini, an annotation assistant for ESC\/Java. In: Oliveira, J.N., Zave, P. (eds.) FME 2001. LNCS, vol.\u00a02021, p. 500. Springer, Heidelberg (2001)"},{"key":"6_CR13","series-title":"SIGPLAN","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 2002)","author":"C. Flanagan","year":"2002","unstructured":"Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation (PLDI 2002), New York. SIGPLAN, vol.\u00a037(5), pp. 234\u2013245. ACM Press, New York (2002)"},{"key":"6_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/3-540-44829-2_8","volume-title":"Model Checking Software","author":"A. Groce","year":"2003","unstructured":"Groce, A., Visser, W.: What went wrong: Explaining counterexamples. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol.\u00a02648, pp. 121\u2013135. Springer, Heidelberg (2003)"},{"key":"6_CR15","first-page":"465","volume-title":"Proceedings of the 18th IFIP Information Security Conference","author":"E. Hubbers","year":"2003","unstructured":"Hubbers, E., Oostdijk, M., Poll, E.: From finite state machines to provably correct java card applets. In: Gritzalis, D., di Vimercati, S.D.C., Samarati, P., Katsikas, S.K. (eds.) Proceedings of the 18th IFIP Information Security Conference, pp. 465\u2013470. Kluwer Academic Publishers, Dordrecht (2003)"},{"key":"6_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1007\/978-3-540-39866-0_23","volume-title":"Perspectives of System Informatics","author":"E.-M. Hubbers","year":"2004","unstructured":"Hubbers, E.-M.: Integrating Tools for Automatic Program Verification. In: Broy, M., Zamulin, A.V. (eds.) PSI 2003. LNCS, vol.\u00a02890, pp. 214\u2013221. Springer, Heidelberg (2004)"},{"key":"6_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/978-3-540-39881-3_19","volume-title":"Security in Pervasive Computing","author":"E.-M. Hubbers","year":"2004","unstructured":"Hubbers, E.-M., Oostdijk, M., Poll, E.: Implementing a Formally Verifiable Security Protocol in Java Card. In: Hutter, D., et al. (eds.) Security in Pervasive Computing. LNCS, vol.\u00a02802, pp. 213\u2013226. Springer, Heidelberg (2004), http:\/\/www.dfki.de\/SPC2003\/"},{"key":"6_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/978-3-540-39656-7_11","volume-title":"Formal Methods for Components and Objects","author":"G.T. Leavens","year":"2003","unstructured":"Leavens, G.T., Cheon, Y., Clifton, C., Ruby, C., Cok, D.R.: How the design of JML accommodates both runtime assertion checking and formal verification. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2002. LNCS, vol.\u00a02852, pp. 262\u2013284. Springer, Heidelberg (2003)"},{"key":"6_CR19","first-page":"105","volume-title":"OOPSLA 2000 Companion","author":"G.T. Leavens","year":"2000","unstructured":"Leavens, G.T., Leino, K.R.M., Poll, E., Ruby, C., Jacobs, B.: JML: notations and tools supporting detailed design in Java. In: OOPSLA 2000 Companion, Minneapolis, Minnesota, pp. 105\u2013106. ACM, New York (2000)"},{"key":"6_CR20","unstructured":"Leavens, G.T., Poll, E., Clifton, C., Cheon, Y., Ruby, C., Cok, D.R., Kiniry, J.: JML reference manual. Department of Computer Science. Iowa State University (April 2003), Available from, http:\/\/www.jmlspecs.org"},{"key":"6_CR21","doi-asserted-by":"crossref","unstructured":"Leino, K.R.M., Millstein, T., Saxe, J.B.: Generating error traces from verification-condition counterexamples. Science of Computer Programming (2004) (to appear)","DOI":"10.1016\/j.scico.2004.05.016"},{"key":"6_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"302","DOI":"10.1007\/BFb0026441","volume-title":"Compiler Construction","author":"K.R.M. Leino","year":"1998","unstructured":"Leino, K.R.M., Nelson, G.: An extended static checker for Modula-3. In: Koskimies, K. (ed.) CC 1998. LNCS, vol.\u00a01383, pp. 302\u2013305. Springer, Heidelberg (1998)"},{"key":"6_CR23","unstructured":"Leino, K.R.M., Nelson, G., Saxe, J.B.: ESC\/Java user\u2019s manual. Technical note, Compaq Systems Research Center (October 2000)"},{"key":"6_CR24","series-title":"SIGPLAN","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1145\/512529.512559","volume-title":"Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation (PLDI 2002)","author":"K.R.M. Leino","year":"2002","unstructured":"Leino, K.R.M., Poetzsch-Heffter, A., Zhou, Y.: Using data groups to specify and check side effects. In: Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation (PLDI 2002), New York. SIGPLAN, vol.\u00a037(5), pp. 246\u2013257. ACM Press, New York (2002)"},{"issue":"1-2","key":"6_CR25","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1016\/j.jlap.2003.07.006","volume":"58","author":"C. March\u00e9","year":"2004","unstructured":"March\u00e9, C., Paulin-Mohring, C., Urbain, X.: The Krakatoa tool for certification of Java\/JavaCard programs annotated in JML. Journal of Logic and Algebraic Programming\u00a058(1-2), 89\u2013106 (2004)","journal-title":"Journal of Logic and Algebraic Programming"},{"key":"6_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1007\/3-540-45418-7_14","volume-title":"Smart Card Programming and Security","author":"H. Meijer","year":"2001","unstructured":"Meijer, H., Poll, E.: Towards a full formal specification of the Java Card. In: Attali, S., Jensen, T. (eds.) E-smart 2001. LNCS, vol.\u00a02140, pp. 165\u2013178. Springer, Heidelberg (2001)"},{"key":"6_CR27","doi-asserted-by":"crossref","unstructured":"Nimmer, J.W., Ernst, M.D.: Static verification of dynamically detected program invariants: Integrating Daikon and ESC\/Java. In: Proceedings, First Workshop on Runtime Verification (RV 2001), Paris, France (July 2001)","DOI":"10.1016\/S1571-0661(04)00256-7"},{"key":"6_CR28","doi-asserted-by":"crossref","unstructured":"Robby, E., Rodr\u00edguez, M.B.: Dwyer, and J. Hatcliff. Checking strong specifications using an extensible software model checking framework. Technical Report SAnToSTR2003- 10. Department of Computing and Information Sciences, Kansas State University (October 2003)","DOI":"10.1007\/978-3-540-24730-2_31"}],"container-title":["Lecture Notes in Computer Science","Construction and Analysis of Safe, Secure, and Interoperable Smart Devices"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-30569-9_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,10,30]],"date-time":"2021-10-30T18:42:11Z","timestamp":1635619331000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-30569-9_6"}},"subtitle":["Progress and Issues in Building and Using ESC\/Java2, Including a Case Study Involving the Use of the Tool to Verify Portions of an Internet Voting Tally System"],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540242871","9783540305699"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-30569-9_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005]]}}}