{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:59:15Z","timestamp":1750309155777,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":15,"publisher":"ACM","license":[{"start":{"date-parts":[[2022,6,7]],"date-time":"2022-06-07T00:00:00Z","timestamp":1654560000000},"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":[[2022,6,7]]},"DOI":"10.1145\/3611096.3611102","type":"proceedings-article","created":{"date-parts":[[2023,10,16]],"date-time":"2023-10-16T23:12:42Z","timestamp":1697497962000},"page":"26-28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Documentation and Educational Materials for a 2nd Edition of the Java Modeling Language"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1864-4974","authenticated-orcid":false,"given":"David R.","family":"Cok","sequence":"first","affiliation":[{"name":"Safer Software Consulting, USA"}]}],"member":"320","published-online":{"date-parts":[[2023,10,16]]},"reference":[{"key":"e_1_3_2_1_1_1","series-title":"Lecture Notes in Computer Science.","volume-title":"Deductive Software Verification \u2013 The KeY Book","author":"Ahrendt Wolfgang","unstructured":"Wolfgang Ahrendt , Bernhard Beckert , Richard Bubel , Reiner H\u00e4hnle , Peter\u00a0 H. Schmitt , and Mattias Ulbrich . 2016. Deductive Software Verification \u2013 The KeY Book . In Lecture Notes in Computer Science. Wolfgang Ahrendt, Bernhard Beckert, Richard Bubel, Reiner H\u00e4hnle, Peter\u00a0H. Schmitt, and Mattias Ulbrich. 2016. Deductive Software Verification \u2013 The KeY Book. In Lecture Notes in Computer Science."},{"volume-title":"High Integrity Software: The SPARK Approach to Safety and Security","author":"Barnes John","key":"e_1_3_2_1_2_1","unstructured":"John Barnes . 2003. High Integrity Software: The SPARK Approach to Safety and Security . Addison Wesley , New York, NY . John Barnes. 2003. High Integrity Software: The SPARK Approach to Safety and Security. Addison Wesley, New York, NY."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.5381\/jot.2004.3.6.a2"},{"key":"e_1_3_2_1_4_1","unstructured":"P. Baudin P.Cuoq J-C. Filli\u00e2tre C. March\u00e9 B. Monate Y. Moy and V. Prevosto. 2008ff. ACSL: ANSI C Specification Language. http:\/\/frama-c.com\/download\/acsl_1.4.pdf.  P. Baudin P.Cuoq J-C. Filli\u00e2tre C. March\u00e9 B. Monate Y. Moy and V. Prevosto. 2008ff. ACSL: ANSI C Specification Language. http:\/\/frama-c.com\/download\/acsl_1.4.pdf."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236454.3236483"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3464971.3468417"},{"key":"e_1_3_2_1_7_1","unstructured":"David\u00a0R. Cok. 2021. OpenJML web site. http:\/\/www.openjml.org  David\u00a0R. Cok. 2021. OpenJML web site. http:\/\/www.openjml.org"},{"key":"e_1_3_2_1_8_1","volume-title":"Java Modeling Language (JML) Reference Manual","author":"Cok R.","unstructured":"David\u00a0 R. Cok , Gary\u00a0 T. Leavens , and Mattias Ulbrich . 2022. Java Modeling Language (JML) Reference Manual , 2 nd edition. In progress. https:\/\/www.openjml.org\/documentation\/JML_Reference_Manual.pdf. David\u00a0R. Cok, Gary\u00a0T. Leavens, and Mattias Ulbrich. 2022. Java Modeling Language (JML) Reference Manual, 2nd edition. In progress. https:\/\/www.openjml.org\/documentation\/JML_Reference_Manual.pdf.","edition":"2"},{"volume-title":"Stainless Verification Framework","author":"EPFL","key":"e_1_3_2_1_9_1","unstructured":"EPFL 2022. Stainless Verification Framework . EPFL , Lausanne, Switzerland . https:\/\/epfl-lara.github.io\/stainless\/intro.html. EPFL 2022. Stainless Verification Framework. EPFL, Lausanne, Switzerland. https:\/\/epfl-lara.github.io\/stainless\/intro.html."},{"key":"e_1_3_2_1_10_1","unstructured":"Frama-C 2007ff. Frama-C web site. https:\/\/frama-c.com.  Frama-C 2007ff. Frama-C web site. https:\/\/frama-c.com."},{"key":"e_1_3_2_1_11_1","unstructured":"Key Project 1998ff. The KeY Project. https:\/\/www.key-project.org  Key Project 1998ff. The KeY Project. https:\/\/www.key-project.org"},{"key":"e_1_3_2_1_12_1","unstructured":"Gary\u00a0T. Leavens. 1997ff. JML web site. http:\/\/www.jmlspecs.org.  Gary\u00a0T. Leavens. 1997ff. JML web site. http:\/\/www.jmlspecs.org."},{"key":"e_1_3_2_1_14_1","volume-title":"July","author":"Leavens T.","year":"2022","unstructured":"Gary\u00a0 T. Leavens , David\u00a0 R. Cok , and Amirfarhad Nilizadeh . 2022. Further Lessons from the JML Project. Accepted to appear , July 2022 . Gary\u00a0T. Leavens, David\u00a0R. Cok, and Amirfarhad Nilizadeh. 2022. Further Lessons from the JML Project. Accepted to appear, July 2022."},{"key":"e_1_3_2_1_15_1","volume-title":"Dafny github site. https:\/\/github.com\/dafny-lang\/dafny. Accessed","author":"M. Leino","year":"2021","unstructured":"K.\u00a0Rustan\u00a0 M. Leino 2021. Dafny github site. https:\/\/github.com\/dafny-lang\/dafny. Accessed September 2021 . K.\u00a0Rustan\u00a0M. Leino 2021. Dafny github site. https:\/\/github.com\/dafny-lang\/dafny. Accessed September 2021."},{"key":"e_1_3_2_1_16_1","unstructured":"K.\u00a0Rustan\u00a0M. Leino Richard\u00a0L. Ford and David\u00a0R. Cok. 2021. Dafny Reference Manual. https:\/\/github.com\/dafny-lang\/dafny\/blob\/master\/docs\/DafnyRef\/out\/DafnyRef.pdf.  K.\u00a0Rustan\u00a0M. Leino Richard\u00a0L. Ford and David\u00a0R. Cok. 2021. Dafny Reference Manual. https:\/\/github.com\/dafny-lang\/dafny\/blob\/master\/docs\/DafnyRef\/out\/DafnyRef.pdf."}],"event":{"name":"FTfJP '22: 24th ACM International Workshop on Formal Techniques for Java-like Programs","acronym":"FTfJP '22","location":"Berlin Germany"},"container-title":["Proceedings of the 24th ACM International Workshop on Formal Techniques for Java-like Programs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3611096.3611102","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3611096.3611102","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T22:50:54Z","timestamp":1750287054000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3611096.3611102"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,6,7]]},"references-count":15,"alternative-id":["10.1145\/3611096.3611102","10.1145\/3611096"],"URL":"https:\/\/doi.org\/10.1145\/3611096.3611102","relation":{},"subject":[],"published":{"date-parts":[[2022,6,7]]},"assertion":[{"value":"2023-10-16","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}