{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,24]],"date-time":"2026-08-24T17:24:50Z","timestamp":1787592290156,"version":"build-2736575974"},"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\/legalcode"}],"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>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.<\/jats:p>\n                  <jats:p>\n                    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.\n                  <\/jats:p>\n                  <jats:p>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.<\/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":[{"vocabulary":"crossref","role":"author"}]},{"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":[{"vocabulary":"crossref","role":"author"}]},{"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":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,4,9]]},"reference":[{"key":"e_1_3_1_2_2","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"e_1_3_1_3_2","unstructured":"AWS Cryptographic Material Providers Library. 2025. https:\/\/github.com\/aws\/aws-cryptographic-material-providerslibrary Accessed: 2025-02-27."},{"key":"e_1_3_1_4_2","unstructured":"AWS Encryption SDK. 2025. https:\/\/github.com\/aws\/aws-encryption-sdk-dafny Accessed: 2025-02-27."},{"key":"e_1_3_1_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/3092703.3092715"},{"key":"e_1_3_1_6_2","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_3_1_7_2","doi-asserted-by":"publisher","unstructured":"Franck Cassez. 2021. Verification of the Incremental Merkle Tree Algorithm with Dafny. In Formal Methods. 445\u2013462. doi:10.1007\/978-3-030-90870-6_24","DOI":"10.1007\/978-3-030-90870-6_24"},{"key":"e_1_3_1_8_2","doi-asserted-by":"publisher","unstructured":"Franck Cassez Joanne Fuller Milad K. Ghale David J. Pearce and Horacio M.A. Quiles. 2023. Formal and Executable Semantics of the Ethereum Virtual Machine in Dafny. In Formal Methods. 571\u2013583. doi:10.1007\/978-3-031-27481-7_32","DOI":"10.1007\/978-3-031-27481-7_32"},{"key":"e_1_3_1_9_2","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. doi:10.1007\/978-3-031-15008-1_5","DOI":"10.1007\/978-3-031-15008-1_5"},{"key":"e_1_3_1_10_2","doi-asserted-by":"publisher","unstructured":"Aleksandar Chakarov Aleksandr Fedchin Zvonimir Rakamari\u0107 and Neha Rungta. 2022. Better Counterexamples for Dafny. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 404\u2013411. doi:10.1007\/978-3-030-99524-9_23","DOI":"10.1007\/978-3-030-99524-9_23"},{"key":"e_1_3_1_11_2","unstructured":"Dafny. 2025. https:\/\/github.com\/dafny-lang\/dafny Accessed: 2025-02-27."},{"key":"e_1_3_1_12_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_1_13_2","doi-asserted-by":"publisher","unstructured":"Antoine Delignat-Lavaud C\u00e9dric Fournet Bryan Parno Jonathan Protzenko Tahina Ramananandro Jay Bosamiya Joseph Lallemand Itsaka Rakotonirina and Yi Zhou. 2021. A Security Model and Fully Verified Implementation for the IETF QUIC Record Layer. In 2021 IEEE Symposium on Security and Privacy (SP). 1162\u20131178. doi:10.1109\/SP40001.2021.00039","DOI":"10.1109\/SP40001.2021.00039"},{"key":"e_1_3_1_14_2","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. doi:10.1007\/978-3-031-33170-1_24","DOI":"10.1007\/978-3-031-33170-1_24"},{"key":"e_1_3_1_15_2","doi-asserted-by":"publisher","unstructured":"Yu Feng Ruben Martins Yuepeng Wang Isil Dillig and Thomas W Reps. 2017. Component-Based Synthesis for Complex APIs. In Symposium on Principles of Programming Languages. 599\u2013612. doi:10.1145\/3009837.3009851","DOI":"10.1145\/3009837.3009851"},{"key":"e_1_3_1_16_2","doi-asserted-by":"publisher","unstructured":"Artifact for Paper \"Metamorph: Synthesizing Large Objects from Dafny Specifications\". 2025. doi:10.5281\/zenodo.14925936 Accessed: 2025-02-27.","DOI":"10.5281\/zenodo.14925936"},{"key":"e_1_3_1_17_2","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. doi:10.1007\/978-3-319-55696-3_17","DOI":"10.1007\/978-3-319-55696-3_17"},{"key":"e_1_3_1_18_2","doi-asserted-by":"publisher","unstructured":"Sumit Gulwani Susmit Jha Ashish Tiwari and Ramarathnam Venkatesan. 2011. Synthesis of Loop-Free Programs. In Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation. 62\u201373. doi:10.1145\/1993498.1993506","DOI":"10.1145\/1993498.1993506"},{"key":"e_1_3_1_19_2","doi-asserted-by":"publisher","unstructured":"Zheng Guo David Cao Davin Tjong Jean Yang Cole Schlesinger and Nadia Polikarpova. 2022. Type-Directed Program Synthesis for RESTful APIs. In International Conference on Programming Language Design and Implementation. 122\u2013136. doi:10.1145\/3519939.3523450","DOI":"10.1145\/3519939.3523450"},{"key":"e_1_3_1_20_2","doi-asserted-by":"publisher","unstructured":"Sankha Narayan Guria Jeffrey S. Foster and David Van Horn. 2023. Absynthe: Abstract Interpretation-Guided Synthesis. In Proceedings of the ACM on Programming Languages Vol. 7. 1584\u20131607. doi:10.1145\/3591285","DOI":"10.1145\/3591285"},{"key":"e_1_3_1_21_2","doi-asserted-by":"publisher","unstructured":"Tihomir Gvero Viktor Kuncak Ivan Kuraj and Ruzica Piskac. 2013. Complete Completion Using Types and Weights. In Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation. 27\u201338. doi:10.1145\/2491956.2462192","DOI":"10.1145\/2491956.2462192"},{"key":"e_1_3_1_22_2","doi-asserted-by":"publisher","unstructured":"Ahmed Irfan Sorawee Porncharoenwase Zvonimir Rakamari\u0107 Neha Rungta and Emina Torlak. 2022. Testing Dafny (Experience Paper). In International Symposium on Software Testing and Analysis. 556\u2013567. doi:10.1145\/3533767.3534382","DOI":"10.1145\/3533767.3534382"},{"key":"e_1_3_1_23_2","doi-asserted-by":"publisher","unstructured":"Shachar Itzhaky Hila Peleg Nadia Polikarpova Reuben NS Rowe and Ilya Sergey. 2021. Cyclic Program Synthesis. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation. 944\u2013959. doi:10.1145\/3453483.3454087","DOI":"10.1145\/3453483.3454087"},{"key":"e_1_3_1_24_2","doi-asserted-by":"publisher","unstructured":"Naman Jain Skanda Vaidyanath Arun Iyer Nagarajan Natarajan Suresh Parthasarathy Sriram Rajamani and Rahul Sharma. 2022. Jigsaw: Large Language Models Meet Program Synthesis. In Proceedings of the 44th International Conference on Software Engineering. 1219\u20131231. doi:10.1145\/3510003.3510203","DOI":"10.1145\/3510003.3510203"},{"key":"e_1_3_1_25_2","doi-asserted-by":"publisher","unstructured":"Jinwoo Kim Qinheping Hu Loris D\u2019Antoni and Thomas Reps. 2021. Semantics-Guided Synthesis. In Proceedings of the ACM on Programming Languages Vol. 5. doi:10.1145\/3434311","DOI":"10.1145\/3434311"},{"key":"e_1_3_1_26_2","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_3_1_27_2","doi-asserted-by":"publisher","DOI":"10.1145\/3586037"},{"key":"e_1_3_1_28_2","doi-asserted-by":"publisher","unstructured":"K Rustan M Leino. 2010. Dafny: An Automatic Program Verifier for Functional Correctness. In International Conference on Logic for Programming Artificial Intelligence and Reasoning. 348\u2013370. doi:10.1007\/978-3-642-17511-4_20","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"e_1_3_1_29_2","doi-asserted-by":"publisher","DOI":"10.1109\/MS.2017.4121212"},{"key":"e_1_3_1_30_2","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384646"},{"key":"e_1_3_1_31_2","volume-title":"Master\u2019s thesis","author":"Martins Hugo Rafael Fecha","year":"2022","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_3_1_32_2","doi-asserted-by":"publisher","DOI":"10.1145\/3563310"},{"key":"e_1_3_1_33_2","doi-asserted-by":"publisher","unstructured":"Md Rakib Hossain Misu Cristina V. Lopes Iris Ma and James Noble. 2024. Towards AI-Assisted Synthesis of Verified Dafny Methods. In Proceedings of the ACM on Software Engineering Vol. 1. 812\u2013835. doi:10.1145\/3643763","DOI":"10.1145\/3643763"},{"key":"e_1_3_1_34_2","doi-asserted-by":"publisher","unstructured":"Daye Nam Baishakhi Ray Seohyun Kim Xianshan Qu and Satish Chandra. 2022. Predictive Synthesis of API-Centric Code. In International Symposium on Machine Programming. 40\u201349. doi:10.1145\/3520312.3534866","DOI":"10.1145\/3520312.3534866"},{"key":"e_1_3_1_35_2","unstructured":"David J. Pearce. 2022. Formalising a Simple Virtual Machine. https:\/\/whileydave.com\/2022\/06\/28\/formalising-asimple-virtual-machine\/ Accessed: 2024-10-15."},{"key":"e_1_3_1_36_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-018-0456-4"},{"key":"e_1_3_1_37_2","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908093"},{"key":"e_1_3_1_38_2","doi-asserted-by":"publisher","DOI":"10.1145\/3290385"},{"key":"e_1_3_1_39_2","doi-asserted-by":"publisher","unstructured":"Kia Rahmani Mohammad Raza Sumit Gulwani Vu Le Daniel Morris Arjun Radhakrishna Gustavo Soares and Ashish Tiwari. 2021. Multi-Modal Program Inference: A Marriage of Pre-Trained Language Models and Component-Based Synthesis. In Proceedings of the ACM on Programming Languages Vol. 5. 1\u201329. doi:10.1145\/3485535","DOI":"10.1145\/3485535"},{"key":"e_1_3_1_40_2","doi-asserted-by":"publisher","unstructured":"Armando Solar-Lezama Liviu Tancau Rastislav Bodik Sanjit Seshia and Vijay Saraswat. 2006. Combinatorial Sketching for Finite Programs. In Proceedings of the 12th International Conference on Architectural Support for Programming Languages and Operating Systems. 404\u2013415. doi:10.1145\/1168857.1168907","DOI":"10.1145\/1168857.1168907"},{"key":"e_1_3_1_41_2","doi-asserted-by":"publisher","unstructured":"Saurabh Srivastava Sumit Gulwani and Jeffrey S Foster. 2010. From Program Verification to Program Synthesis. In Proceedings of the ACM on Programming Languages. 313\u2013326. doi:10.1145\/1706299.1706337","DOI":"10.1145\/1706299.1706337"},{"key":"e_1_3_1_42_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-65112-0_7"},{"key":"e_1_3_1_43_2","doi-asserted-by":"publisher","DOI":"10.1051\/wujns\/2021266481"},{"key":"e_1_3_1_44_2","unstructured":"Z3. 2025. https:\/\/github.com\/Z3Prover\/z3 Accessed: 2025-02-27."},{"key":"e_1_3_1_45_2","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":[[2026,8,24]],"date-time":"2026-08-24T16:29:46Z","timestamp":1787588986000},"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":[{"value":"2475-1421","type":"electronic"}],"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"}}]}}