{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,23]],"date-time":"2026-10-23T20:31:03Z","timestamp":1792787463063,"version":"4.5.0"},"publisher-location":"New York, NY, USA","reference-count":84,"publisher":"ACM","license":[{"start":{"date-parts":[[2026,10,3]],"date-time":"2026-10-03T00:00:00Z","timestamp":1790985600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"funder":[{"name":"U.S. Department of Energy","award":["DE-SC0024467"],"award-info":[{"award-number":["DE-SC0024467"]}],"id":[{"id":"https:\/\/ror.org\/01bj3aw27","id-type":"ROR","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2026,10,4]]},"DOI":"10.1145\/3822455.3830309","type":"proceedings-article","created":{"date-parts":[[2026,9,11]],"date-time":"2026-09-11T16:18:48Z","timestamp":1789143528000},"page":"116-127","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Anvil: An Empirical Study of LLM-Powered Alloy Synthesis, Validation, and Repair"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0008-9382-9091","authenticated-orcid":false,"given":"Yang","family":"Hong","sequence":"first","affiliation":[{"name":"University of Texas at Austin, Austin, TX, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0002-5733-6878","authenticated-orcid":false,"given":"Chenbo","family":"Yin","sequence":"additional","affiliation":[{"name":"University of Texas at Austin, Austin, TX, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0002-0466-1028","authenticated-orcid":false,"given":"Shan","family":"Jiang","sequence":"additional","affiliation":[{"name":"University of Texas at Austin, Austin, TX, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0009-6680-6190","authenticated-orcid":false,"given":"Yulei","family":"Fu","sequence":"additional","affiliation":[{"name":"University of Texas at Austin, Austin, TX, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0009-7424-7819","authenticated-orcid":false,"given":"Sarfraz","family":"Khurshid","sequence":"additional","affiliation":[{"name":"University of Texas at Austin, Austin, TX, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,10,3]]},"reference":[{"key":"e_1_3_3_2_2_2","unstructured":"Mohannad Alhanahnah Md\u00a0Rashedul Hasan and Hamid Bagheri. 2024. An Empirical Evaluation of Pre-trained Large Language Models for Repairing Declarative Formal Specifications. arxiv:https:\/\/arXiv.org\/abs\/2404.11050arXiv 2404.11050."},{"key":"e_1_3_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"e_1_3_3_2_4_2","doi-asserted-by":"crossref","unstructured":"Ramakrishna Bairi et\u00a0al. 2024. CodePlan: Repository-Level Coding using LLMs and Planning. Proc. ACM Softw. Eng. 1 FSE Article 31 (July 2024) 24\u00a0pages.","DOI":"10.1145\/3643757"},{"key":"e_1_3_3_2_5_2","unstructured":"Rastislav Bod\u00edk and Barbara Jobstmann. 2013. Algorithmic program synthesis: Introduction. STTT (2013)."},{"key":"e_1_3_3_2_6_2","doi-asserted-by":"crossref","unstructured":"Stefano Ceri Georg Gottlob Letizia Tanca et\u00a0al. 1989. What you always wanted to know about Datalog (and never dared to ask). IEEE transactions on knowledge and data engineering 1 1 (1989) 146\u2013166.","DOI":"10.1109\/69.43410"},{"key":"e_1_3_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.18653\/v1\/2023.findings-emnlp.614"},{"key":"e_1_3_3_2_8_2","unstructured":"Mark Chen et\u00a0al. 2021. Evaluating Large Language Models Trained on Code. arXiv preprint arXiv:https:\/\/arXiv.org\/abs\/2107.03374 (2021)."},{"key":"e_1_3_3_2_9_2","doi-asserted-by":"crossref","unstructured":"Malinda Dilhara et\u00a0al. 2024. Unprecedented Code Change Automation: The Fusion of LLMs and Transformation by Example. Proc. ACM Softw. Eng. 1 FSE (2024) 631\u2013653.","DOI":"10.1145\/3643755"},{"key":"e_1_3_3_2_10_2","doi-asserted-by":"crossref","unstructured":"Madeline Endres et\u00a0al. 2024. Can Large Language Models Transform Natural Language Intent into Formal Method Postconditions?Proc. ACM Softw. Eng. 1 FSE Article 84 (July 2024) 24\u00a0pages.","DOI":"10.1145\/3660791"},{"key":"e_1_3_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009851"},{"key":"e_1_3_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737977"},{"key":"e_1_3_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/1062455.1062535"},{"key":"e_1_3_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1145\/2568225.2568250"},{"key":"e_1_3_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.5555\/1987389.1987408"},{"key":"e_1_3_3_2_16_2","volume-title":"Larch: Languages and tools for formal specification","author":"Guttag John\u00a0V","year":"2012","unstructured":"John\u00a0V Guttag and James\u00a0J Horning. 2012. Larch: Languages and tools for formal specification. Springer Science & Business Media."},{"key":"e_1_3_3_2_17_2","volume-title":"CAV","author":"Gvero Tihomir","year":"2011","unstructured":"Tihomir Gvero, Viktor Kuncak, and Ruzica Piskac. 2011. Interactive Synthesis of Code Snippets. In CAV."},{"key":"e_1_3_3_2_18_2","unstructured":"Md\u00a0Rashedul Hasan et\u00a0al. 2023. Automated Repair of Declarative Software Specifications in the Era of Large Language Models. arxiv:https:\/\/arXiv.org\/abs\/2310.12425arXiv 2310.12425."},{"key":"e_1_3_3_2_19_2","unstructured":"Yang Hong et\u00a0al. 2025. On the effectiveness of large language models in writing alloy formulas. arXiv preprint arXiv:https:\/\/arXiv.org\/abs\/2502.15441 (2025)."},{"key":"e_1_3_3_2_20_2","volume-title":"SPIN","author":"Hua Jinru","year":"2017","unstructured":"Jinru Hua and Sarfraz Khurshid. 2017. EdSketch: Execution-Driven Sketching for Java. In SPIN."},{"key":"e_1_3_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1145\/3597503.3639223"},{"key":"e_1_3_3_2_22_2","doi-asserted-by":"crossref","unstructured":"Daniel Jackson. 2002. Alloy: A Lightweight Object Modelling Notation. TSE (2002).","DOI":"10.1145\/505145.505149"},{"key":"e_1_3_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45500-0_25"},{"key":"e_1_3_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/347324.383378"},{"key":"e_1_3_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/2786805.2803189"},{"key":"e_1_3_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/1806799.1806833"},{"key":"e_1_3_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1145\/3786583.3786873"},{"key":"e_1_3_3_2_28_2","unstructured":"Shan Jiang Zijian Yi and Chenguang Zhu. 2026. Semantic Voting: Execution-Grounded Consensus for LLM Code Generation. arXiv preprint arXiv:https:\/\/arXiv.org\/abs\/2605.08680 (2026)."},{"key":"e_1_3_3_2_29_2","unstructured":"Shan Jiang Zijian Yi and Chenguang Zhu. 2026. Sketch-and-Verify: Structured Inference-Time Scaling via Program Sketching. arXiv preprint arXiv:https:\/\/arXiv.org\/abs\/2605.08658 (2026)."},{"key":"e_1_3_3_2_30_2","unstructured":"Shan Jiang Chenguang Zhu and Sarfraz Khurshid. 2024. Generating executable oracles to check conformance of client code to requirements of JDK Javadocs using LLMs. CoRR abs\/2411.01789 (2024). arXiv:https:\/\/arXiv.org\/abs\/2411.01789"},{"key":"e_1_3_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1145\/3798204"},{"key":"e_1_3_3_2_32_2","doi-asserted-by":"crossref","unstructured":"Zhihan Jiang et\u00a0al. 2024. LILAC: Log Parsing using LLMs with Adaptive Parsing Cache. Proc. ACM Softw. Eng. 1 FSE Article 7 (July 2024) 24\u00a0pages.","DOI":"10.1145\/3643733"},{"key":"e_1_3_3_2_33_2","doi-asserted-by":"crossref","unstructured":"Xin Jin and Zhiqiang Lin. 2024. SimLLM: Calculating Semantic Similarity in Code Summaries using a Large Language Model-Based Approach. Proc. ACM Softw. Eng. 1 FSE Article 62 (July 2024) 24\u00a0pages.","DOI":"10.1145\/3660769"},{"key":"e_1_3_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.5555\/94062"},{"key":"e_1_3_3_2_35_2","doi-asserted-by":"crossref","unstructured":"Sungmin Kang Gabin An and Shin Yoo. 2024. A Quantitative and Qualitative Evaluation of LLM-Based Explainable Fault Localization. Proc. ACM Softw. Eng. 1 FSE Article 64 (July 2024) 23\u00a0pages.","DOI":"10.1145\/3660771"},{"key":"e_1_3_3_2_36_2","first-page":"272","volume-title":"SAT","author":"Khurshid Sarfraz","year":"2003","unstructured":"Sarfraz Khurshid et\u00a0al. 2003. A Case for Efficient Solution Enumeration. In SAT. 272\u2013286."},{"key":"e_1_3_3_2_37_2","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509555"},{"key":"e_1_3_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.1145\/1806596.1806632"},{"key":"e_1_3_3_2_39_2","first-page":"404","volume-title":"Formal Underpinnings of Java Workshop (at OOPSLA\u201998)","author":"Leavens Gary\u00a0T","year":"1998","unstructured":"Gary\u00a0T Leavens, Albert\u00a0L Baker, and Clyde Ruby. 1998. JML: A Java modeling language. In Formal Underpinnings of Java Workshop (at OOPSLA\u201998). Citeseer, 404\u2013420."},{"key":"e_1_3_3_2_40_2","doi-asserted-by":"publisher","DOI":"10.1145\/3597503.3639180"},{"key":"e_1_3_3_2_41_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-43652-3_31"},{"key":"e_1_3_3_2_42_2","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065018"},{"key":"e_1_3_3_2_43_2","volume-title":"MODELS","author":"Maoz Shahar","year":"2011","unstructured":"Shahar Maoz, Jan\u00a0Oliver Ringert, and Bernhard Rumpe. 2011. CD2Alloy: Class Diagrams Analysis Using Alloy Revisited. In MODELS."},{"key":"e_1_3_3_2_44_2","doi-asserted-by":"publisher","DOI":"10.5555\/2032497.2032515"},{"key":"e_1_3_3_2_45_2","doi-asserted-by":"publisher","DOI":"10.5555\/872023.872551"},{"key":"e_1_3_3_2_46_2","doi-asserted-by":"publisher","DOI":"10.1145\/1985793.1985863"},{"key":"e_1_3_3_2_47_2","doi-asserted-by":"crossref","unstructured":"Fangwen Mu et\u00a0al. 2024. ClarifyGPT: A Framework for Enhancing LLM-Based Code Generation via Requirements Clarification. Proc. ACM Softw. Eng. 1 FSE Article 103 (July 2024) 23\u00a0pages.","DOI":"10.1145\/3660810"},{"key":"e_1_3_3_2_48_2","doi-asserted-by":"publisher","DOI":"10.1145\/3597503.3639187"},{"key":"e_1_3_3_2_49_2","volume-title":"LISA","author":"Nelson Timothy","year":"2010","unstructured":"Timothy Nelson et\u00a0al. 2010. The Margrave Tool for Firewall Analysis. In LISA."},{"key":"e_1_3_3_2_50_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2013.6606569"},{"key":"e_1_3_3_2_51_2","doi-asserted-by":"publisher","DOI":"10.1145\/3106237.3106272"},{"key":"e_1_3_3_2_52_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14107-2_27"},{"key":"e_1_3_3_2_53_2","volume-title":"An introduction to Prolog","author":"Nugues Pierre\u00a0M","year":"2006","unstructured":"Pierre\u00a0M Nugues. 2006. An introduction to Prolog. Springer."},{"key":"e_1_3_3_2_54_2","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2738007"},{"key":"e_1_3_3_2_55_2","doi-asserted-by":"crossref","unstructured":"Daniel Perelman et\u00a0al. 2014. Test-driven Synthesis. PLDI (2014).","DOI":"10.1145\/2594291.2594297"},{"key":"e_1_3_3_2_56_2","doi-asserted-by":"publisher","DOI":"10.5555\/646243.681607"},{"key":"e_1_3_3_2_57_2","doi-asserted-by":"crossref","unstructured":"Natali Ruchansky and Davide Proserpio. 2013. A (Not) NICE Way to Verify the Openflow Switch Specification: Formal Modelling of the Openflow Switch Using Alloy. SIGCOMM (2013).","DOI":"10.1145\/2486001.2491711"},{"key":"e_1_3_3_2_58_2","doi-asserted-by":"crossref","unstructured":"Gabriel Ryan et\u00a0al. 2024. Code-Aware Prompting: A Study of Coverage-Guided Test Generation in Regression Setting using LLM. Proc. ACM Softw. Eng. 1 FSE Article 43 (July 2024) 21\u00a0pages.","DOI":"10.1145\/3643769"},{"key":"e_1_3_3_2_59_2","doi-asserted-by":"publisher","DOI":"10.5555\/1883978.1884015"},{"key":"e_1_3_3_2_60_2","doi-asserted-by":"crossref","unstructured":"Ilya Shlyakhter. 2001. Generating effective symmetry-breaking predicates for search problems. Electron. Notes Discret. Math. 9 (2001) 19\u201335.","DOI":"10.1016\/S1571-0653(04)00311-7"},{"key":"e_1_3_3_2_61_2","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2003.1240298"},{"key":"e_1_3_3_2_62_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_23"},{"key":"e_1_3_3_2_63_2","doi-asserted-by":"publisher","DOI":"10.1145\/2025113.2025153"},{"key":"e_1_3_3_2_64_2","unstructured":"Armando Solar-Lezama. 2008. Program Synthesis by Sketching. Ph.\u00a0D. Dissertation. University of California Berkeley."},{"key":"e_1_3_3_2_65_2","doi-asserted-by":"publisher","DOI":"10.1145\/1168857.1168907"},{"key":"e_1_3_3_2_66_2","doi-asserted-by":"crossref","unstructured":"Armando Solar-Lezama et\u00a0al. 2007. Sketching Stencils. PLDI (2007).","DOI":"10.1145\/1250734.1250754"},{"key":"e_1_3_3_2_67_2","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375599"},{"key":"e_1_3_3_2_68_2","volume-title":"SPIN","author":"Sullivan Allison","year":"2014","unstructured":"Allison Sullivan et\u00a0al. 2014. Towards a Test Automation Framework for Alloy. In SPIN."},{"key":"e_1_3_3_2_69_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICST.2017.31"},{"key":"e_1_3_3_2_70_2","volume-title":"SQAMIA","author":"Sullivan Allison","year":"2017","unstructured":"Allison Sullivan et\u00a0al. 2017. Evaluating State Modeling Techniques in Alloy. In SQAMIA."},{"key":"e_1_3_3_2_71_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-32409-4_21"},{"key":"e_1_3_3_2_72_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICST.2018.00047"},{"key":"e_1_3_3_2_73_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-68237-0_23"},{"key":"e_1_3_3_2_74_2","doi-asserted-by":"publisher","DOI":"10.5555\/1763507.1763571"},{"key":"e_1_3_3_2_75_2","doi-asserted-by":"crossref","unstructured":"Nalin Wadhwa et\u00a0al. 2024. CORE: Resolving Code Quality Issues using LLMs. Proc. ACM Softw. Eng. 1 FSE Article 36 (July 2024) 23\u00a0pages.","DOI":"10.1145\/3643762"},{"key":"e_1_3_3_2_76_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-91271-4_9"},{"key":"e_1_3_3_2_77_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-91271-4_8"},{"key":"e_1_3_3_2_78_2","doi-asserted-by":"publisher","DOI":"10.1145\/3238147.3238162"},{"key":"e_1_3_3_2_79_2","doi-asserted-by":"publisher","DOI":"10.1145\/3183440.3183488"},{"key":"e_1_3_3_2_80_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE-Companion.2019.00049"},{"key":"e_1_3_3_2_81_2","doi-asserted-by":"crossref","unstructured":"Wei Wang et\u00a0al. 2024. Rocks Coding Not Development: A Human-Centric Experimental Evaluation of LLM-Supported SE Tasks. Proc. ACM Softw. Eng. 1 FSE Article 32 (July 2024) 23\u00a0pages.","DOI":"10.1145\/3643758"},{"key":"e_1_3_3_2_82_2","volume-title":"Proceedings of the 33rd ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC\/FSE 2025","author":"Xia Chunqiu\u00a0Steven","year":"2025","unstructured":"Chunqiu\u00a0Steven Xia et\u00a0al. 2025. Agentless: Demystifying LLM-based Software Engineering Agents. In Proceedings of the 33rd ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC\/FSE 2025. ACM, 24\u00a0pages. To appear."},{"key":"e_1_3_3_2_83_2","volume-title":"ICST","author":"Yang Zijiang","year":"2018","unstructured":"Zijiang Yang et\u00a0al. 2018. Test Execution Driven Synthesis of API Sequences With Conditionals and Loops. In ICST."},{"key":"e_1_3_3_2_84_2","unstructured":"Hua Zhong Shan Jiang and Sarfraz Khurshid. 2025. An approach for API synthesis using large language models. arXiv preprint arXiv:https:\/\/arXiv.org\/abs\/2502.15246 (2025)."},{"key":"e_1_3_3_2_85_2","unstructured":"Hua Zhong Shan Jiang and Sarfraz Khurshid. 2025. APRIL: API Synthesis with Automatic Prompt Optimization and Reinforcement Learning. arXiv preprint arXiv:https:\/\/arXiv.org\/abs\/2509.25196 (2025)."}],"event":{"name":"MODELS 2026: ACM\/IEEE 29th International Conference on Model Driven Engineering Languages and Systems","location":"M\u00e1laga Spain","acronym":"MODELS 2026","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering"]},"container-title":["Proceedings of the ACM\/IEEE 29th International Conference on Model Driven Engineering Languages and Systems"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/abs\/10.1145\/3822455.3830309","content-type":"text\/html","content-version":"vor","intended-application":"syndication"}],"deposited":{"date-parts":[[2026,9,16]],"date-time":"2026-09-16T10:49:55Z","timestamp":1789555795000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3822455.3830309"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,10,3]]},"references-count":84,"alternative-id":["10.1145\/3822455.3830309","10.1145\/3822455"],"URL":"https:\/\/doi.org\/10.1145\/3822455.3830309","relation":{},"subject":[],"published":{"date-parts":[[2026,10,3]]},"assertion":[{"value":"2026-10-03","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}