{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T01:07:57Z","timestamp":1760058477115,"version":"build-2065373602"},"reference-count":44,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA1","license":[{"start":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T00:00:00Z","timestamp":1744156800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,4,9]]},"abstract":"<jats:p>\n            Program synthesis aims to produce code that adheres to user-provided specifications. In this work, we focus on synthesizing sequences of calls to formally specified APIs to generate objects that satisfy certain properties. This problem is particularly relevant in automated test generation, where a test engine may need an object with specific properties to trigger a given execution path. Constructing instances of complex data structures may require dozens of method calls, but reasoning about consecutive calls is computationally expensive, and existing work typically limits the number of calls in the solution.    In this paper, we focus on synthesizing such long sequences of method calls in the Dafny programming language. To that end, we introduce Metamorph, a synthesis tool that uses counterexamples returned by the Dafny verifier to reason about the effects of method calls one at a time, limiting the complexity of solver queries. We also aim to limit the overall number of SMT queries by comparing the counterexamples using two distance metrics we develop for guiding the synthesis process. In particular, we introduce a novel\n            <jats:italic toggle=\"yes\">piecewise distance<\/jats:italic>\n            metric, which puts a provably correct lower bound on the number of method calls in the solution and allows us to frame the synthesis problem as weighted A* search. When computing piecewise distance, we view object states as conjunctions of atomic constraints, identify constraints that each method call can satisfy, and combine this information using integer programming.    We evaluate Metamorph\u2019s ability to generate large objects on six benchmarks defining key data structures: linked lists, queues, arrays, binary trees, and graphs. Metamorph can successfully construct programs that require up to 57 method calls per instance and compares favorably to an alternative baseline approach. Additionally, we integrate Metamorph with DTest, Dafny\u2019s automated test generation toolkit, and show that Metamorph can synthesize test inputs for parts of the AWS Cryptographic Material Providers Library that DTest alone is not able to cover. Finally, we use Metamorph to generate executable bytecode for a simple virtual machine, demonstrating that the techniques described here are more broadly applicable in the context of specification-guided synthesis.\n          <\/jats:p>","DOI":"10.1145\/3720448","type":"journal-article","created":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T13:48:26Z","timestamp":1744206506000},"page":"759-785","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Metamorph: Synthesizing Large Objects from Dafny Specifications"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0810-1941","authenticated-orcid":false,"given":"Aleksandr","family":"Fedchin","sequence":"first","affiliation":[{"name":"Tufts University, Medford, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0009-7458-7864","authenticated-orcid":false,"given":"Alexander Y.","family":"Bai","sequence":"additional","affiliation":[{"name":"Tufts University, Medford, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8043-1166","authenticated-orcid":false,"given":"Jeffrey S.","family":"Foster","sequence":"additional","affiliation":[{"name":"Tufts University, Medford, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,4,9]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","unstructured":"Rajeev Alur Rastislav Bodik 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. In 2013 Formal Methods in Computer-Aided Design. 1\u20138. https:\/\/doi.org\/10.1109\/FMCAD.2013.6679385 10.1109\/FMCAD.2013.6679385","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"e_1_2_1_2_1","unstructured":"AWS Cryptographic Material Providers Library. 2025. https:\/\/github.com\/aws\/aws-cryptographic-material-providers-library Accessed: 2025-02-27"},{"key":"e_1_2_1_3_1","unstructured":"AWS Encryption SDK. 2025. https:\/\/github.com\/aws\/aws-encryption-sdk-dafny Accessed: 2025-02-27"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3092703.3092715"},{"key":"e_1_2_1_5_1","unstructured":"David Brandfonbrener Sibi Raja Tarun Prasad Chloe Loughridge Jianang Yang Simon Henniger William E. Byrd Robert Zinkov and Nada Amin. 2024. Verified Multi-Step Synthesis using Large Language Models and Monte Carlo Tree Search. arxiv:2402.08147."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","unstructured":"Franck Cassez. 2021. Verification of the Incremental Merkle Tree Algorithm with Dafny. In Formal Methods. 445\u2013462. https:\/\/doi.org\/10.1007\/978-3-030-90870-6_24 10.1007\/978-3-030-90870-6_24","DOI":"10.1007\/978-3-030-90870-6_24"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-27481-7_32"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","unstructured":"Franck Cassez Joanne Fuller and Horacio Mijail Ant\u00f3n Quiles. 2022. Deductive Verification of Smart Contracts with Dafny. In Formal Methods for Industrial Critical Systems. 50\u201366. https:\/\/doi.org\/10.1007\/978-3-031-15008-1_5 10.1007\/978-3-031-15008-1_5","DOI":"10.1007\/978-3-031-15008-1_5"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99524-9_23"},{"key":"e_1_2_1_10_1","unstructured":"Dafny. 2025. https:\/\/github.com\/dafny-lang\/dafny Accessed: 2025-02-27"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40001.2021.00039"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","unstructured":"Aleksandr Fedchin Tyler Dean Jeffrey S Foster Eric Mercer Zvonimir Rakamari\u0107 Giles Reger Neha Rungta Robin Salkeld Lucas Wagner and Cassidy Waldrip. 2023. A Toolkit for Automated Testing of Dafny. In NASA Formal Methods. 397\u2013413. https:\/\/doi.org\/10.1007\/978-3-031-33170-1_24 10.1007\/978-3-031-33170-1_24","DOI":"10.1007\/978-3-031-33170-1_24"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009851"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.14925936"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","unstructured":"Stefan Forstenlechner David Fagan Miguel Nicolau and Michael O\u2019Neill. 2017. A Grammar Design Pattern for Arbitrary Program Synthesis Problems in Genetic Programming. In Genetic Programming. 262\u2013277. https:\/\/doi.org\/10.1007\/978-3-319-55696-3_17 10.1007\/978-3-319-55696-3_17","DOI":"10.1007\/978-3-319-55696-3_17"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993506"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523450"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591285"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462192"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3533767.3534382"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454087"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3510003.3510203"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434311"},{"key":"e_1_2_1_25_1","unstructured":"Hugo Krawczyk and Pasi Eronen. 2010. RFC 5869: HMAC-based Extract-and-Expand KDF (HKDF). https:\/\/datatracker.ietf.org\/doc\/html\/rfc5869 Accessed: 2024-10-15"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3586037"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/MS.2017.4121212"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384646"},{"key":"e_1_2_1_30_1","unstructured":"Hugo Rafael Fecha Martins. 2022. Automated Program Repair of Arithmetic Programs in Dafny: Repairing Simple Arithmetic Programs. Master\u2019s thesis. Instituto Superior T\u00e9cnico."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563310"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3643763"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3520312.3534866"},{"key":"e_1_2_1_34_1","unstructured":"David J. Pearce. 2022. Formalising a Simple Virtual Machine. https:\/\/whileydave.com\/2022\/06\/28\/formalising-a-simple-virtual-machine\/ Accessed: 2024-10-15"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-018-0456-4"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908093"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290385"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485535"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/1168857.1168907"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706337"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-65112-0_7"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1051\/wujns\/2021266481"},{"key":"e_1_2_1_43_1","unstructured":"Z3. 2025. https:\/\/github.com\/Z3Prover\/z3 Accessed: 2025-02-27"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3551349.3556951"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3720448","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3720448","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T17:09:10Z","timestamp":1760029750000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3720448"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,4,9]]},"references-count":44,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2025,4,9]]}},"alternative-id":["10.1145\/3720448"],"URL":"https:\/\/doi.org\/10.1145\/3720448","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2025,4,9]]},"assertion":[{"value":"2024-10-16","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-02-18","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-04-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}