{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T02:44:26Z","timestamp":1767926666397,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":42,"publisher":"ACM","license":[{"start":{"date-parts":[[2022,7,18]],"date-time":"2022-07-18T00:00:00Z","timestamp":1658102400000},"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,7,18]]},"DOI":"10.1145\/3533767.3534382","type":"proceedings-article","created":{"date-parts":[[2022,7,15]],"date-time":"2022-07-15T14:28:50Z","timestamp":1657895330000},"page":"556-567","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":15,"title":["Testing Dafny (experience paper)"],"prefix":"10.1145","author":[{"given":"Ahmed","family":"Irfan","sequence":"first","affiliation":[{"name":"Amazon Web Services, USA"}]},{"given":"Sorawee","family":"Porncharoenwase","sequence":"additional","affiliation":[{"name":"University of Washington, USA"}]},{"given":"Zvonimir","family":"Rakamari\u0107","sequence":"additional","affiliation":[{"name":"Amazon Web Services, USA"}]},{"given":"Neha","family":"Rungta","sequence":"additional","affiliation":[{"name":"Amazon Web Services, USA"}]},{"given":"Emina","family":"Torlak","sequence":"additional","affiliation":[{"name":"Amazon Web Services, USA"}]}],"member":"320","published-online":{"date-parts":[[2022,7,18]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"[n. d.]. AWS Batch: Fully managed processing at any scale. https:\/\/aws.amazon.com\/batch\/ Accessed: 2022-01-07 \t\t\t\t\t  [n. d.]. AWS Batch: Fully managed processing at any scale. https:\/\/aws.amazon.com\/batch\/ Accessed: 2022-01-07"},{"key":"e_1_3_2_1_2_1","volume-title":"Syntax-guided synthesis","author":"Alur Rajeev","unstructured":"Rajeev Alur , Rastislav Bod\u00edk , Garvit Juniwal , Milo M. K. Martin , Mukund Raghothaman , Sanjit A. Seshia , Rishabh Singh , Armando Solar-Lezama , Emina Torlak , and Abhishek Udupa . 2013. Syntax-guided synthesis . IEEE. https:\/\/ieeexplore.ieee.org\/document\/6679385\/ Rajeev Alur, Rastislav Bod\u00edk, Garvit Juniwal, Milo M. K. Martin, Mukund Raghothaman, Sanjit A. Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak, and Abhishek Udupa. 2013. Syntax-guided synthesis. IEEE. https:\/\/ieeexplore.ieee.org\/document\/6679385\/"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3439802"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.3233\/978-1-58603-929-5-825"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8_11"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96142-2_6"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1670412.1670413"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2889160.2889206"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-68446-4_14"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3363562"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28891-3_12"},{"key":"e_1_3_2_1_12_1","unstructured":"[n. d.]. Dafny. https:\/\/github.com\/dafny-lang\/dafny \t\t\t\t\t  [n. d.]. Dafny. https:\/\/github.com\/dafny-lang\/dafny"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3127323"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132782"},{"key":"e_1_3_2_1_15_1","volume-title":"Reference: Racket","author":"Flatt Matthew","year":"2010","unstructured":"Matthew Flatt and PLT. 2010 . Reference: Racket . PLT Design Inc .. Matthew Flatt and PLT. 2010. Reference: Racket. PLT Design Inc.."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-011-1793-7_4"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3064176.3064183"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/QRS54544.2021.00032"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1561\/2500000010"},{"key":"e_1_3_2_1_20_1","volume-title":"14th USENIX Symposium on Operating Systems Design and Implementation (OSDI 20)","author":"Hance Travis","year":"2020","unstructured":"Travis Hance , Andrea Lattuada , Chris Hawblitzel , Jon Howell , Rob Johnson , and Bryan Parno . 2020 . Storage Systems are Distributed Systems (So Verify Them That Way!) . In 14th USENIX Symposium on Operating Systems Design and Implementation (OSDI 20) . USENIX Association, 99\u2013115. isbn:978-1-939133-19-9 https:\/\/www.usenix.org\/conference\/osdi20\/presentation\/hance Travis Hance, Andrea Lattuada, Chris Hawblitzel, Jon Howell, Rob Johnson, and Bryan Parno. 2020. Storage Systems are Distributed Systems (So Verify Them That Way!). In 14th USENIX Symposium on Operating Systems Design and Implementation (OSDI 20). USENIX Association, 99\u2013115. isbn:978-1-939133-19-9 https:\/\/www.usenix.org\/conference\/osdi20\/presentation\/hance"},{"key":"e_1_3_2_1_21_1","unstructured":"William Gallard Hatch Pierce Darragh Guy Watson and Eric Eide. 2020. Xsmith software repository. https:\/\/gitlab.flux.utah.edu\/xsmith\/xsmith \t\t\t\t\t  William Gallard Hatch Pierce Darragh Guy Watson and Eric Eide. 2020. Xsmith software repository. https:\/\/gitlab.flux.utah.edu\/xsmith\/xsmith"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815428"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-34968-4_13"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21668-3_22"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2017.8115669"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-21437-0_14"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3293882.3330553"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11086-005-0008-6"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"e_1_3_2_1_31_1","unstructured":"K. Rustan M. Leino Richard L. Ford and David R. Cok. [n. d.]. Dafny Reference Manual. https:\/\/dafny-lang.github.io\/dafny\/DafnyRef\/DafnyRef \t\t\t\t\t  K. Rustan M. Leino Richard L. Ford and David R. Cok. [n. d.]. Dafny Reference Manual. https:\/\/dafny-lang.github.io\/dafny\/DafnyRef\/DafnyRef"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9155-4"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3368089.3409763"},{"key":"e_1_3_2_1_34_1","first-page":"100","article-title":"Differential Testing for Software","volume":"10","author":"McKeeman William M.","year":"1998","unstructured":"William M. McKeeman . 1998 . Differential Testing for Software . Digit. Tech. J. , 10 , 1 (1998), 100 \u2013 107 . http:\/\/www.hpl.hp.com\/hpjournal\/dtj\/vol10num1\/vol10num1art9.pdf William M. McKeeman. 1998. Differential Testing for Software. Digit. Tech. J., 10, 1 (1998), 100\u2013107. http:\/\/www.hpl.hp.com\/hpjournal\/dtj\/vol10num1\/vol10num1art9.pdf","journal-title":"Digit. Tech. J."},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485529"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-63618-0_5"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3368826.3377927"},{"key":"e_1_3_2_1_38_1","unstructured":"The Xsmith team. [n. d.]. Personal communication. \t\t\t\t\t  The Xsmith team. [n. d.]. Personal communication."},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594340"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428261"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385985"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993532"}],"event":{"name":"ISSTA '22: 31st ACM SIGSOFT International Symposium on Software Testing and Analysis","location":"Virtual South Korea","acronym":"ISSTA '22","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering"]},"container-title":["Proceedings of the 31st ACM SIGSOFT International Symposium on Software Testing and Analysis"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3533767.3534382","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3533767.3534382","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T18:43:40Z","timestamp":1750272220000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3533767.3534382"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,7,18]]},"references-count":42,"alternative-id":["10.1145\/3533767.3534382","10.1145\/3533767"],"URL":"https:\/\/doi.org\/10.1145\/3533767.3534382","relation":{},"subject":[],"published":{"date-parts":[[2022,7,18]]},"assertion":[{"value":"2022-07-18","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}