{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,13]],"date-time":"2026-02-13T10:15:57Z","timestamp":1770977757342,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":13,"publisher":"ACM","license":[{"start":{"date-parts":[[2021,7,11]],"date-time":"2021-07-11T00:00:00Z","timestamp":1625961600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100002081","name":"Irish Research Council","doi-asserted-by":"publisher","award":["GOIPG\/2019\/4529"],"award-info":[{"award-number":["GOIPG\/2019\/4529"]}],"id":[{"id":"10.13039\/501100002081","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2021,7,13]]},"DOI":"10.1145\/3464971.3468422","type":"proceedings-article","created":{"date-parts":[[2021,7,8]],"date-time":"2021-07-08T22:07:03Z","timestamp":1625782023000},"page":"32-38","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Using dafny to solve the VerifyThis 2021 challenges"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7708-3877","authenticated-orcid":false,"given":"Marie","family":"Farrell","sequence":"first","affiliation":[{"name":"Maynooth University, Ireland"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6598-5512","authenticated-orcid":false,"given":"Conor","family":"Reynolds","sequence":"additional","affiliation":[{"name":"Maynooth University, Ireland"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3886-4675","authenticated-orcid":false,"given":"Rosemary","family":"Monahan","sequence":"additional","affiliation":[{"name":"Maynooth University, Ireland"}]}],"member":"320","published-online":{"date-parts":[[2021,7,11]]},"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","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31762-0_2"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-021-00619-x"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-30446-1_25"},{"key":"e_1_3_2_1_6_1","volume-title":"International Symposium on Artificial Intelligence, Robotics and Automation in Space. ESA.","author":"Farrell Marie","year":"2020","unstructured":"Marie Farrell , Nikos Mavrakis , Clare Dixon , and Yang Gao . 2020 . Formal Verification of an Autonomous Grasping Algorithm . In International Symposium on Artificial Intelligence, Robotics and Automation in Space. ESA. Marie Farrell, Nikos Mavrakis, Clare Dixon, and Yang Gao. 2020. Formal Verification of an Autonomous Grasping Algorithm. In International Symposium on Artificial Intelligence, Robotics and Automation in Space. ESA."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-015-0396-8"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-016-0438-x"},{"key":"e_1_3_2_1_9_1","volume-title":"VerifyThis 2017: A Program Verification Competition (Karlsruhe Reports in Informatics)","author":"Huisman Marieke","unstructured":"Marieke Huisman , Rosemary Monahan , Peter M\u00fcller , Wojciech Mostowski , and Mattias Ulbrich . 2017. VerifyThis 2017: A Program Verification Competition (Karlsruhe Reports in Informatics) . Karlsruhe Institute of Technology . Marieke Huisman, Rosemary Monahan, Peter M\u00fcller, Wojciech Mostowski, and Mattias Ulbrich. 2017. VerifyThis 2017: A Program Verification Competition (Karlsruhe Reports in Informatics). Karlsruhe Institute of Technology."},{"key":"e_1_3_2_1_10_1","unstructured":"Marieke Huisman Rosemary Monahan Peter M\u00fcller Andrei Paskevich and Gidon Ernst. 2019. VerifyThis 2018: A Program Verification Competition. Universit\u00e9 Paris-Saclay.  Marieke Huisman Rosemary Monahan Peter M\u00fcller Andrei Paskevich and Gidon Ernst. 2019. VerifyThis 2018: A Program Verification Competition. Universit\u00e9 Paris-Saclay."},{"key":"e_1_3_2_1_11_1","unstructured":"Marieke Huisman Rosemary Monahan Peter Muller and Erik Poll. 2016. VerifyThis 2016: A program verification competition.  Marieke Huisman Rosemary Monahan Peter Muller and Erik Poll. 2016. VerifyThis 2016: A program verification competition."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-21437-0_14"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17511-4_20"}],"event":{"name":"ISSTA '21: 30th ACM SIGSOFT International Symposium on Software Testing and Analysis","location":"Virtual Denmark","acronym":"ISSTA '21","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 23rd ACM International Workshop on Formal Techniques for Java-like Programs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3464971.3468422","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3464971.3468422","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:18:25Z","timestamp":1750191505000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3464971.3468422"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,7,11]]},"references-count":13,"alternative-id":["10.1145\/3464971.3468422","10.1145\/3464971"],"URL":"https:\/\/doi.org\/10.1145\/3464971.3468422","relation":{},"subject":[],"published":{"date-parts":[[2021,7,11]]},"assertion":[{"value":"2021-07-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}