{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:34:26Z","timestamp":1750307666070,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":21,"publisher":"ACM","license":[{"start":{"date-parts":[[2009,3,8]],"date-time":"2009-03-08T00:00:00Z","timestamp":1236470400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2009,3,8]]},"DOI":"10.1145\/1529282.1529373","type":"proceedings-article","created":{"date-parts":[[2009,4,15]],"date-time":"2009-04-15T13:37:11Z","timestamp":1239802631000},"page":"404-408","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["Executing JML specifications of Java card applications"],"prefix":"10.1145","author":[{"given":"N\u00e9stor","family":"Cata\u00f1o","sequence":"first","affiliation":[{"name":"University of Madeira, Funchal, Portugal"}]},{"given":"Tim","family":"Wahls","sequence":"additional","affiliation":[{"name":"Dickinson College, Carlisle, PA"}]}],"member":"320","published-online":{"date-parts":[[2009,3,8]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Electronic Notes in Theoretical Computer Science","volume":"64","author":"Abdennadher S.","year":"2002"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/11526841_7"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2004.05.011"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.5555\/2932433.2932497"},{"key":"e_1_3_2_1_6_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"272","DOI":"10.1007\/3-540-45614-7_16","volume-title":"L.-H","author":"Cata\u00f1o N.","year":"2002"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.5555\/646542.696202"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1292316.1292322"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/1025115.1025231"},{"key":"e_1_3_2_1_10_1","unstructured":"The ESC\/Java 2 Tool. http:\/\/secure.ucd.ie\/products\/opensource\/ESCJava2\/.  The ESC\/Java 2 Tool. http:\/\/secure.ucd.ie\/products\/opensource\/ESCJava2\/."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"crossref","unstructured":"W.\n       \n      Grieskamp\n    .\n      \n  \n   \n  A computation model for Z based on concurrent constraint resolution. In J. P. Bowen S. Dunne A. Galloway and S. King editors ZB 2000: Formal Specification and Development in Z and B First International Conference of Z and B Users volume \n  1878\n   of \n  Lecture Notes in Computer Science pages \n  414\n  --\n  432 York UK September \n  2000\n  . \n  Springer-Verlag\n  .   W. Grieskamp. A computation model for Z based on concurrent constraint resolution. In J. P. Bowen S. Dunne A. Galloway and S. King editors ZB 2000: Formal Specification and Development in Z and B First International Conference of Z and B Users volume 1878 of Lecture Notes in Computer Science pages 414--432 York UK September 2000. Springer-Verlag.","DOI":"10.1007\/3-540-44525-0_24"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1049\/sej.1989.0045"},{"key":"e_1_3_2_1_13_1","unstructured":"The JACK Tool. http:\/\/www-sop.inria.fr\/eve-rest\/soft\/Jack\/jack.html.  The JACK Tool. http:\/\/www-sop.inria.fr\/eve-rest\/soft\/Jack\/jack.html."},{"volume-title":"Massachusetts Institute of Technology","year":"2006","author":"Jackson D.","key":"e_1_3_2_1_14_1"},{"key":"e_1_3_2_1_15_1","unstructured":"Java Card Technology. http:\/\/java.sun.com\/products\/javacard\/.  Java Card Technology. http:\/\/java.sun.com\/products\/javacard\/."},{"key":"e_1_3_2_1_16_1","unstructured":"The Krakatoa Tool. http:\/\/krakatoa.lri.fr\/.  The Krakatoa Tool. http:\/\/krakatoa.lri.fr\/."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"crossref","unstructured":"B.\n       \n      Krause\n     and \n      \n      \n      T.\n       \n      Wahls\n      \n  \n  . \n  jmle: A tool for executing JML specifications via constraint programming. In L. Brim editor Formal Methods for Industrial Critical Systems (FMICS '06) volume \n  4346\n   of \n  Lecture Notes in Computer Science pages \n  293\n  --\n  296\n  . \n  Springer-Verlag August \n  2006\n  .   B. Krause and T. Wahls. jmle: A tool for executing JML specifications via constraint programming. In L. Brim editor Formal Methods for Industrial Critical Systems (FMICS '06) volume 4346 of Lecture Notes in Computer Science pages 293--296. Springer-Verlag August 2006.","DOI":"10.1007\/978-3-540-70952-7_19"},{"key":"e_1_3_2_1_18_1","unstructured":"G. T. Leavens. The Java Modeling Language (JML) home page. http:\/\/www.jmlspecs.org.  G. T. Leavens. The Java Modeling Language (JML) home page. http:\/\/www.jmlspecs.org."},{"volume-title":"Morgan Kaufmann","year":"2003","author":"Link J.","key":"e_1_3_2_1_19_1"},{"key":"e_1_3_2_1_20_1","unstructured":"Microsoft Research. Executable specifications: Creating testable enforceable designs February 2001. http:\/\/research.microsoft.com\/foundations\/-ESpecTesting.doc.  Microsoft Research. Executable specifications: Creating testable enforceable designs February 2001. http:\/\/research.microsoft.com\/foundations\/-ESpecTesting.doc."},{"volume-title":"MIT Press","year":"2001","author":"Robinson A.","key":"e_1_3_2_1_22_1"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/646485.694447"}],"event":{"name":"SAC09: The 2009 ACM Symposium on Applied Computing","sponsor":["SIGAPP ACM Special Interest Group on Applied Computing"],"location":"Honolulu Hawaii","acronym":"SAC09"},"container-title":["Proceedings of the 2009 ACM symposium on Applied Computing"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1529282.1529373","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1529282.1529373","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T13:29:33Z","timestamp":1750253373000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1529282.1529373"}},"subtitle":["a case study"],"short-title":[],"issued":{"date-parts":[[2009,3,8]]},"references-count":21,"alternative-id":["10.1145\/1529282.1529373","10.1145\/1529282"],"URL":"https:\/\/doi.org\/10.1145\/1529282.1529373","relation":{},"subject":[],"published":{"date-parts":[[2009,3,8]]},"assertion":[{"value":"2009-03-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}