{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:47:04Z","timestamp":1772164024063,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":9,"publisher":"ACM","license":[{"start":{"date-parts":[[2012,12,2]],"date-time":"2012-12-02T00:00:00Z","timestamp":1354406400000},"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":[[2012,12,2]]},"DOI":"10.1145\/2402676.2402682","type":"proceedings-article","created":{"date-parts":[[2012,11,29]],"date-time":"2012-11-29T12:08:34Z","timestamp":1354190914000},"page":"9-10","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":10,"title":["Developing verified programs with Dafny"],"prefix":"10.1145","author":[{"given":"K. Rustan M.","family":"Leino","sequence":"first","affiliation":[{"name":"Microsoft Research, Redmond, WA, USA"}]}],"member":"320","published-online":{"date-parts":[[2012,12,2]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"crossref","unstructured":"L.\n      Herbert K. R. M.\n      Leino and \n      J.\n      Quaresma\n  . \n  Using Dafny an automatic program verifier\n  . In B. Meyer and M. Nordio editors LASER \n  2012 volume \n  7682\n   of \n  LNCS pages \n  156\n  --\n  181\n  . \n  Springer 2012.  L. Herbert K. R. M. Leino and J. Quaresma. Using Dafny an automatic program verifier. In B. Meyer and M. Nordio editors LASER 2012 volume 7682 of LNCS pages 156--181. Springer 2012.","DOI":"10.1007\/978-3-642-35746-6_6"},{"key":"e_1_3_2_1_2_1","volume-title":"VS-Tools workshop at VSTTE 2010","author":"Jacobs B.","year":"2010","unstructured":"B. Jacobs , J. Smans , and F. Piessens . VeriFast: Imperative programs as proofs . In VS-Tools workshop at VSTTE 2010 , Aug. 2010 . B. Jacobs, J. Smans, and F. Piessens. VeriFast: Imperative programs as proofs. In VS-Tools workshop at VSTTE 2010, Aug. 2010."},{"key":"e_1_3_2_1_3_1","series-title":"NATO Science for Peace and Security Series D: Information and Communication Security","first-page":"152","volume-title":"Software Safety and Security: Tools for Analysis and Verification","author":"Koenig J.","year":"2012","unstructured":"J. Koenig and K. R. M. Leino . Getting started with Dafny: A guide . In T. Nipkow, O. Grumberg, and B. Hauptmann, editors, Software Safety and Security: Tools for Analysis and Verification , volume 33 of NATO Science for Peace and Security Series D: Information and Communication Security , pages 152 -- 181 . IOS Press , 2012 . Summer School Marktoberdorf 2011 lecture notes. J. Koenig and K. R. M. Leino. Getting started with Dafny: A guide. In T. Nipkow, O. Grumberg, and B. Hauptmann, editors, Software Safety and Security: Tools for Analysis and Verification, volume 33 of NATO Science for Peace and Security Series D: Information and Communication Security, pages 152--181. IOS Press, 2012. Summer School Marktoberdorf 2011 lecture notes."},{"key":"e_1_3_2_1_4_1","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"407","DOI":"10.1007\/978-3-642-24690-6_28","volume-title":"Software Engineering and Formal Methods - 9th International Conference, SEFM","author":"Le Goues C.","year":"2011","unstructured":"C. Le Goues , K. R. M. Leino , and M. Moskal . The Boogie Verification Debugger (tool paper) . In G. Barthe, A. Pardo, and G. Schneider, editors, Software Engineering and Formal Methods - 9th International Conference, SEFM 2011 , volume 7041 of LNCS , pages 407 -- 414 . Springer , Nov. 2011. C. Le Goues, K. R. M. Leino, and M. Moskal. The Boogie Verification Debugger (tool paper). In G. Barthe, A. Pardo, and G. Schneider, editors, Software Engineering and Formal Methods - 9th International Conference, SEFM 2011, volume 7041 of LNCS, pages 407--414. Springer, Nov. 2011."},{"key":"e_1_3_2_1_5_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. R. M.","year":"2009","unstructured":"K. R. M. Leino . Specification and verification of object-oriented software . In M. Broy, W. Sitou, and T. 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. R. M. Leino. Specification and verification of object-oriented software. In M. Broy, W. Sitou, and T. 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_6_1","doi-asserted-by":"crossref","unstructured":"K. R. M.\n      Leino\n    .\n  Dafny: An automatic program verifier for functional correctness\n  . In E. M. Clarke and A. Voronkov editors LPAR-16 volume \n  6355\n   of \n  LNCS pages \n  348\n  --\n  370\n  . \n  Springer Apr. \n  2010\n  .   K. R. M. Leino. Dafny: An automatic program verifier for functional correctness. In E. M. Clarke and A. Voronkov editors LPAR-16 volume 6355 of LNCS pages 348--370. Springer Apr. 2010.","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27940-9_21"},{"key":"e_1_3_2_1_8_1","volume-title":"Usable auto-active verification","author":"Leino K. R. M.","year":"2010","unstructured":"K. R. M. Leino and M. Moskal . Usable auto-active verification . In T. Ball, L. Zuck, and N. Shankar, editors, UV10 (Usable Verification) workshop. http:\/\/fm.csl.sri.com\/UV10\/, Nov. 2010 . K. R. M. Leino and M. Moskal. Usable auto-active verification. In T. Ball, L. Zuck, and N. Shankar, editors, UV10 (Usable Verification) workshop. http:\/\/fm.csl.sri.com\/UV10\/, Nov. 2010."},{"key":"e_1_3_2_1_9_1","series-title":"Series in Computer Science","volume-title":"Object-oriented Software Construction","author":"Meyer B.","year":"1988","unstructured":"B. Meyer . Object-oriented Software Construction . Series in Computer Science . Prentice-Hall International , 1988 . B. Meyer. Object-oriented Software Construction. Series in Computer Science. Prentice-Hall International, 1988."}],"event":{"name":"HILT'12: ACM SIGAda Annual","location":"Boston Massachusetts USA","acronym":"HILT'12","sponsor":["SIGAda ACM Special Interest Group on Ada Programming Language","SIGAPP ACM Special Interest Group on Applied Computing","SIGPLAN ACM Special Interest Group on Programming Languages","SIGBED ACM Special Interest Group on Embedded Systems","SIGCAS ACM Special Interest Group on Computers and Society","SIGCSE ACM Special Interest Group on Computer Science Education"]},"container-title":["Proceedings of the 2012 ACM conference on High integrity language technology"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2402676.2402682","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2402676.2402682","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T05:48:12Z","timestamp":1750225692000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2402676.2402682"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,12,2]]},"references-count":9,"alternative-id":["10.1145\/2402676.2402682","10.1145\/2402676"],"URL":"https:\/\/doi.org\/10.1145\/2402676.2402682","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/2402709.2402682","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2012,12,2]]},"assertion":[{"value":"2012-12-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}