{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,5]],"date-time":"2026-10-05T22:38:52Z","timestamp":1791239932127,"version":"4.1.0"},"publisher-location":"New York, NY, USA","reference-count":16,"publisher":"ACM","license":[{"start":{"date-parts":[[2010,3,28]],"date-time":"2010-03-28T00:00:00Z","timestamp":1269734400000},"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":[[2010,3,28]]},"DOI":"10.1145\/1868281.1868289","type":"proceedings-article","created":{"date-parts":[[2010,10,12]],"date-time":"2010-10-12T15:38:31Z","timestamp":1286897911000},"page":"1-8","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Specifying generic Java programs"],"prefix":"10.1145","author":[{"given":"Alain","family":"Giorgetti","sequence":"first","affiliation":[{"name":"Univ. of Franche-Comt\u00e9, INRIA Nancy - Grand Est, Villers-l\u00e8s-Nancy"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Claude","family":"March\u00e9","sequence":"additional","affiliation":[{"name":"Univ. Paris-Sud, Orsay"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Elena","family":"Tushkanova","sequence":"additional","affiliation":[{"name":"Univ. of Franche-Comt\u00e9, INRIA Nancy - Grand Est, Villers-l\u00e8s-Nancy"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Olga","family":"Kouchnarenko","sequence":"additional","affiliation":[{"name":"Univ. of Franche-Comt\u00e9, INRIA Nancy - Grand Est, Villers-l\u00e8s-Nancy"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2010,3,28]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"ACSL: ANSI\/ISO C Specification Language, version 1.4","author":"Baudin P.","year":"2009","unstructured":"}} P. Baudin , J.-C. Filli\u00e2tre , C. March\u00e9 , B. Monate , Y. Moy , and V. Prevosto . ACSL: ANSI\/ISO C Specification Language, version 1.4 , 2009 . http:\/\/frama-c.cea.fr\/acsl.html. }}P. Baudin, J.-C. Filli\u00e2tre, C. March\u00e9, B. Monate, Y. Moy, and V. Prevosto. ACSL: ANSI\/ISO C Specification Language, version 1.4, 2009. http:\/\/frama-c.cea.fr\/acsl.html."},{"key":"e_1_3_2_1_2_1","series-title":"ENTCS","first-page":"73","volume-title":"FMICS 03","author":"Burdy L.","year":"2003","unstructured":"}} L. Burdy , Y. Cheon , D. Cok , M. Ernst , J. Kiniry , G. Leavens , K. Leino , and E. Poll . An Overview of JML Tools and Applications . In FMICS 03 , volume 80 of ENTCS , pages 73 -- 89 . Elsevier , 2003 . }}L. Burdy, Y. Cheon, D. Cok, M. Ernst, J. Kiniry, G. Leavens, K. Leino, and E. Poll. An Overview of JML Tools and Applications. In FMICS 03, volume 80 of ENTCS, pages 73--89. Elsevier, 2003."},{"key":"e_1_3_2_1_3_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"270","DOI":"10.1007\/10930755_18","volume-title":"TPHOLs'03","author":"Chrzaszcz J.","year":"2003","unstructured":"}} J. Chrzaszcz . Implementing modules in the Coq system . In TPHOLs'03 , volume 2758 of Lecture Notes in Computer Science , pages 270 -- 286 . Springer , 2003 . }}J. Chrzaszcz. Implementing modules in the Coq system. In TPHOLs'03, volume 2758 of Lecture Notes in Computer Science, pages 270--286. Springer, 2003."},{"key":"e_1_3_2_1_4_1","first-page":"27","volume-title":"SAVCBS '08","author":"Cok D. R.","year":"2008","unstructured":"}} D. R. Cok . Adapting JML to generic types and Java 1.6 . In SAVCBS '08 , pages 27 -- 34 , 2008 . }}D. R. Cok. Adapting JML to generic types and Java 1.6. In SAVCBS '08, pages 27--34, 2008."},{"key":"e_1_3_2_1_5_1","volume-title":"Theorem Proving in Higher Order Logics: Emerging Trends","author":"Filli\u00e2tre J.-C.","year":"1999","unstructured":"}} J.-C. Filli\u00e2tre and N. Magaud . Certification of sorting algorithms in the Coq system . In Theorem Proving in Higher Order Logics: Emerging Trends , 1999 . }}J.-C. Filli\u00e2tre and N. Magaud. Certification of sorting algorithms in the Coq system. In Theorem Proving in Higher Order Logics: Emerging Trends, 1999."},{"key":"e_1_3_2_1_6_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1007\/978-3-540-73368-3_21","volume-title":"CAV'07","author":"Filli\u00e2tre J.-C.","year":"2007","unstructured":"}} J.-C. Filli\u00e2tre and C. March\u00e9 . The Why\/Krakatoa\/Caduceus platform for deductive program verification . In CAV'07 , volume 4590 of Lecture Notes in Computer Science , pages 173 -- 177 . Springer , July 2007 . }}J.-C. Filli\u00e2tre and C. March\u00e9. The Why\/Krakatoa\/Caduceus platform for deductive program verification. In CAV'07, volume 4590 of Lecture Notes in Computer Science, pages 173--177. Springer, July 2007."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1596627.1596634"},{"key":"e_1_3_2_1_8_1","volume-title":"Design by Contract with JML. Available from http:\/\/www.jmlspecs.org","author":"Leavens G. T.","year":"2006","unstructured":"}} G. T. Leavens and Y. Cheon . Design by Contract with JML. Available from http:\/\/www.jmlspecs.org , 2006 . }}G. T. Leavens and Y. Cheon. Design by Contract with JML. Available from http:\/\/www.jmlspecs.org, 2006."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/2391276.2391291"},{"key":"e_1_3_2_1_10_1","volume-title":"Winter School on Object-Oriented Verification","author":"March\u00e9 C.","year":"2009","unstructured":"}} C. March\u00e9 . The Krakatoa tool for deductive verification of Java programs . Winter School on Object-Oriented Verification , Viinistu, Estonia , Jan. 2009 . http:\/\/krakatoa.lri.fr\/ws\/. }}C. March\u00e9. The Krakatoa tool for deductive verification of Java programs. Winter School on Object-Oriented Verification, Viinistu, Estonia, Jan. 2009. http:\/\/krakatoa.lri.fr\/ws\/."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/99583.99620"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1297027.1297053"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-79980-1_24"},{"key":"e_1_3_2_1_15_1","volume-title":"Formal Verification of Object-Oriented Software, Papers Presented at the International Conference","author":"Tafat A.","year":"2010","unstructured":"}} A. Tafat , S. Boulm\u00e9 , and C. March\u00e9 . A refinement methodology for object-oriented programs . In Formal Verification of Object-Oriented Software, Papers Presented at the International Conference , Paris , France, June 2010 . }}A. Tafat, S. Boulm\u00e9, and C. March\u00e9. A refinement methodology for object-oriented programs. In Formal Verification of Object-Oriented Software, Papers Presented at the International Conference, Paris, France, June 2010."},{"key":"e_1_3_2_1_16_1","volume-title":"July","author":"Development Team The Coq","year":"2006","unstructured":"}} The Coq Development Team . The Coq Proof Assistant Reference Manual - Version V8.1 , July 2006 . http:\/\/coq.inria.fr. }}The Coq Development Team. The Coq Proof Assistant Reference Manual - Version V8.1, July 2006. http:\/\/coq.inria.fr."},{"key":"e_1_3_2_1_17_1","volume-title":"Fakult\u00e4t f\u00fcr Informatik","author":"Ulbrich M.","year":"2007","unstructured":"}} M. Ulbrich . Software verification for Java 5. Diplomarbeit , Fakult\u00e4t f\u00fcr Informatik , Universit\u00e4t Karlsruhe , 2007 . }}M. Ulbrich. Software verification for Java 5. Diplomarbeit, Fakult\u00e4t f\u00fcr Informatik, Universit\u00e4t Karlsruhe, 2007."}],"event":{"name":"LDTA '10: Language Descriptions, Tools and Applications","location":"Paphos Cyprus","acronym":"LDTA '10","sponsor":["University of Minnesota Software Engineering Center","SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the Tenth Workshop on Language Descriptions, Tools and Applications"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1868281.1868289","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1868281.1868289","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T12:08:52Z","timestamp":1750248532000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1868281.1868289"}},"subtitle":["two case studies"],"short-title":[],"issued":{"date-parts":[[2010,3,28]]},"references-count":16,"alternative-id":["10.1145\/1868281.1868289","10.1145\/1868281"],"URL":"https:\/\/doi.org\/10.1145\/1868281.1868289","relation":{},"subject":[],"published":{"date-parts":[[2010,3,28]]},"assertion":[{"value":"2010-03-28","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}