{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:46:17Z","timestamp":1772163977330,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":10,"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.2402689","type":"proceedings-article","created":{"date-parts":[[2012,11,29]],"date-time":"2012-11-29T12:08:34Z","timestamp":1354190914000},"page":"25-26","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Program proving using intermediate verification languages (IVLs) like boogie and why3"],"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":"publisher","DOI":"10.1007\/11804192_17"},{"key":"e_1_3_2_1_2_1","volume-title":"BOOGIE 2011: First International Workshop on Intermediate Verification Languages","author":"Bobot F.","year":"2011","unstructured":"F. Bobot , J.-C. Filli\u00e2tre , C. March\u00e9 , and A. Paskevich . Why3: Shepherd your herd of provers . In BOOGIE 2011: First International Workshop on Intermediate Verification Languages , Aug. 2011 . F. Bobot, J.-C. Filli\u00e2tre, C. March\u00e9, and A. Paskevich. Why3: Shepherd your herd of provers. In BOOGIE 2011: First International Workshop on Intermediate Verification Languages, Aug. 2011."},{"key":"e_1_3_2_1_3_1","volume-title":"University Paris-Sud","author":"Filli\u00e2tre J.-C.","year":"2011","unstructured":"J.-C. Filli\u00e2tre . Deductive program verification. Habilitation thesis , University Paris-Sud 11, Dec. 2011 . J.-C. Filli\u00e2tre. Deductive program verification. Habilitation thesis, University Paris-Sud 11, Dec. 2011."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27705-4_8"},{"key":"e_1_3_2_1_5_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":"Computer Aided Verification, 19th International Conference, CAV","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 W. Damm and H. Hermanns, editors, Computer Aided Verification, 19th International Conference, CAV 2007 , 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 W. Damm and H. Hermanns, editors, Computer Aided Verification, 19th International Conference, CAV 2007, volume 4590 of Lecture Notes in Computer Science, pages 173--177. Springer, July 2007."},{"key":"e_1_3_2_1_6_1","series-title":"Lecture Notes in Computer Science","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 Lecture Notes in Computer Science , 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 Lecture Notes in Computer Science, pages 407--414. Springer, Nov. 2011."},{"key":"e_1_3_2_1_7_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_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","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12002-2_26"},{"key":"e_1_3_2_1_11_1","series-title":"NATO Science for Peace and Security Series D: Information and Communication Security","first-page":"351","volume-title":"Software Safety and Security","author":"Leino K. R. M.","year":"2007","unstructured":"K. R. M. Leino and W. Schulte . A verifying compiler for a multi-threaded object-oriented language . In M. Broy, J. Gr\u00fcnbauer, and T. Hoare, editors, Software Safety and Security , volume 9 of NATO Science for Peace and Security Series D: Information and Communication Security , pages 351 -- 416 . IOS Press , 2007 . Summer School Marktoberdorf 2006 lecture notes. K. R. M. Leino and W. Schulte. A verifying compiler for a multi-threaded object-oriented language. In M. Broy, J. Gr\u00fcnbauer, and T. Hoare, editors, Software Safety and Security, volume 9 of NATO Science for Peace and Security Series D: Information and Communication Security, pages 351--416. IOS Press, 2007. Summer School Marktoberdorf 2006 lecture notes."}],"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.2402689","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2402676.2402689","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.2402689"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,12,2]]},"references-count":10,"alternative-id":["10.1145\/2402676.2402689","10.1145\/2402676"],"URL":"https:\/\/doi.org\/10.1145\/2402676.2402689","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/2402709.2402689","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"}}]}}