{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,16]],"date-time":"2026-06-16T23:07:05Z","timestamp":1781651225485,"version":"3.54.5"},"publisher-location":"New York, NY, USA","reference-count":15,"publisher":"ACM","license":[{"start":{"date-parts":[[2015,7,7]],"date-time":"2015-07-07T00:00:00Z","timestamp":1436227200000},"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":[[2015,7,7]]},"DOI":"10.1145\/2786536.2786542","type":"proceedings-article","created":{"date-parts":[[2015,7,6]],"date-time":"2015-07-06T14:04:29Z","timestamp":1436191469000},"page":"1-5","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Automatic verification of Dafny programs with traits"],"prefix":"10.1145","author":[{"given":"Reza","family":"Ahmadi","sequence":"first","affiliation":[{"name":"University of Tampere"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"K. Rustan M.","family":"Leino","sequence":"additional","affiliation":[{"name":"Microsoft Research"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jyrki","family":"Nummenmaa","sequence":"additional","affiliation":[{"name":"University of Tampere"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2015,7,7]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/11804192_17"},{"key":"e_1_3_2_1_2_1","unstructured":"C# Language Specification. ECMA International June 2006. C# Language Specification. ECMA International June 2006."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512558"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/11924661_17"},{"key":"e_1_3_2_1_5_1","volume-title":"The Java Language Specification","author":"Gosling James","year":"1996","unstructured":"James Gosling , Bill Joy , and Guy Steele . The Java Language Specification . Addison-Wesley , 1996 . James Gosling, Bill Joy, and Guy Steele. The Java Language Specification. Addison-Wesley, 1996."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2187671.2187678"},{"key":"e_1_3_2_1_7_1","series-title":"LNCS","first-page":"156","volume-title":"Tools for Practical Software Verification, LASER, International Summer School","author":"Herbert Luke","year":"2011","unstructured":"Luke Herbert , K. Rustan M. Leino , and Jose Quaresma . Using Dafny, an automatic program verifier . In Bertrand Meyer and Martin Nordio, editors, Tools for Practical Software Verification, LASER, International Summer School 2011 , volume 7682 of LNCS , pages 156 -- 181 . Springer , 2012. Luke Herbert, K. Rustan M. Leino, and Jose Quaresma. Using Dafny, an automatic program verifier. In Bertrand Meyer and Martin Nordio, editors, Tools for Practical Software Verification, LASER, International Summer School 2011, volume 7682 of LNCS, pages 156--181. Springer, 2012."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/11813040_19"},{"key":"e_1_3_2_1_9_1","series-title":"NATO Science for Peace and Security Series D: Information and Communication Security","first-page":"231","volume-title":"Engineering Methods and Tools for Software Safety and Security","author":"Leino K. Rustan M.","year":"2009","unstructured":"K. Rustan M. Leino . Specification and verification of object-oriented software . In Manfred Broy, Wassiou Sitou, and Tony Hoare, editors, Engineering Methods and Tools for Software Safety and Security , volume 22 of NATO Science for Peace and Security Series D: Information and Communication Security , pages 231 -- 266 . IOS Press , 2009 . Summer School Marktoberdorf 2008 lecture notes. K. Rustan M. Leino. Specification and verification of object-oriented software. In Manfred Broy, Wassiou Sitou, and Tony Hoare, editors, Engineering Methods and Tools for Software Safety and Security, volume 22 of NATO Science for Peace and Security Series D: Information and Communication Security, pages 231--266. IOS Press, 2009. Summer School Marktoberdorf 2008 lecture notes."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"crossref","unstructured":"K. Rustan M.\n      Leino\n  . \n  Dafny: An automatic program verifier for functional correctness\n  . In Edmund M. Clarke and Andrei Voronkov editors LPAR-16 volume \n  6355\n   of \n  LNCS pages \n  348\n  --\n  370\n  . \n  Springer April \n  2010\n  .   K. Rustan M. Leino. Dafny: An automatic program verifier for functional correctness. In Edmund M. Clarke and Andrei Voronkov editors LPAR-16 volume 6355 of LNCS pages 348--370. Springer April 2010.","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"e_1_3_2_1_11_1","first-page":"1488","volume-title":"35th International Conference on Software Engineering, ICSE '13","author":"Leino K. Rustan M.","year":"2013","unstructured":"K. Rustan M. Leino . Developing verified programs with Dafny. In David Notkin, Betty H. C. Cheng, and Klaus Pohl, editors , 35th International Conference on Software Engineering, ICSE '13 , pages 1488 -- 1490 . IEEE\/ACM, May 2013 . K. Rustan M. Leino. Developing verified programs with Dafny. In David Notkin, Betty H. C. Cheng, and Klaus Pohl, editors, 35th International Conference on Software Engineering, ICSE '13, pages 1488--1490. IEEE\/ACM, May 2013."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/197320.197383"},{"key":"e_1_3_2_1_13_1","series-title":"Series in Computer Science","volume-title":"Object-oriented Software Construction","author":"Meyer Bertrand","year":"1988","unstructured":"Bertrand Meyer . Object-oriented Software Construction . Series in Computer Science . Prentice-Hall International , 1988 . Bertrand Meyer. Object-oriented Software Construction. Series in Computer Science. Prentice-Hall International, 1988."},{"key":"e_1_3_2_1_14_1","series-title":"Series in Innovative Technology","volume-title":"Systems Programming with Modula-3","author":"Nelson Greg","year":"1991","unstructured":"Greg Nelson , editor. Systems Programming with Modula-3 . Series in Innovative Technology . Prentice-Hall , 1991 . Greg Nelson, editor. Systems Programming with Modula-3. Series in Innovative Technology. Prentice-Hall, 1991."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_53"}],"event":{"name":"ECOOP '15: European Conference on Object-Oriented Programming ECOOP 2015","location":"Prague Czech Republic","acronym":"ECOOP '15","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGSOFT ACM Special Interest Group on Software Engineering"]},"container-title":["Proceedings of the 17th Workshop on Formal Techniques for Java-like Programs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2786536.2786542","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2786536.2786542","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T05:07:41Z","timestamp":1750223261000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2786536.2786542"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,7,7]]},"references-count":15,"alternative-id":["10.1145\/2786536.2786542","10.1145\/2786536"],"URL":"https:\/\/doi.org\/10.1145\/2786536.2786542","relation":{},"subject":[],"published":{"date-parts":[[2015,7,7]]},"assertion":[{"value":"2015-07-07","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}