{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,18]],"date-time":"2026-07-18T06:04:08Z","timestamp":1784354648945,"version":"3.55.0"},"reference-count":68,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"7","license":[{"start":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T00:00:00Z","timestamp":1782864000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T00:00:00Z","timestamp":1782864000000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T00:00:00Z","timestamp":1782864000000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"funder":[{"name":"National Science Foundation","award":["CCF-1755890"],"award-info":[{"award-number":["CCF-1755890"]}]},{"name":"National Science Foundation","award":["CCF-1618132"],"award-info":[{"award-number":["CCF-1618132"]}]},{"name":"National Science Foundation","award":["CCF-2139845"],"award-info":[{"award-number":["CCF-2139845"]}]},{"name":"National Science Foundation","award":["CCF-2124116"],"award-info":[{"award-number":["CCF-2124116"]}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IIEEE Trans. Software Eng."],"published-print":{"date-parts":[[2026,7]]},"DOI":"10.1109\/tse.2026.3682711","type":"journal-article","created":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T19:58:34Z","timestamp":1775851114000},"page":"2064-2075","source":"Crossref","is-referenced-by-count":0,"title":["Automated Repair of Alloy Specifications in the Era of Large Language Models"],"prefix":"10.1109","volume":"52","author":[{"ORCID":"https:\/\/orcid.org\/0009-0009-3417-4352","authenticated-orcid":false,"given":"Md Rashedul","family":"Hasan","sequence":"first","affiliation":[{"name":"School of Computing, University of Nebraska-Lincoln, Lincoln, NE, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4434-4812","authenticated-orcid":false,"given":"Jiawei","family":"Li","sequence":"additional","affiliation":[{"name":"Donald Bren School of Information and Computer Science, University of California, Irvine, CA, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8221-5352","authenticated-orcid":false,"given":"Iftekhar","family":"Ahmed","sequence":"additional","affiliation":[{"name":"Donald Bren School of Information and Computer Science, University of California, Irvine, CA, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6686-466X","authenticated-orcid":false,"given":"Hamid","family":"Bagheri","sequence":"additional","affiliation":[{"name":"School of Computing, University of Nebraska-Lincoln, Lincoln, NE, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"263","reference":[{"key":"ref1","volume-title":"Software Abstractions - Logic, Language, and Analysis.","author":"Jackson","year":"2006"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1145\/503209.503219"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1145\/2371401.2371416"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2010.01.049"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1145\/2568225.2568291"},{"key":"ref6","first-page":"1522","article-title":"Reducing run-time adaptation space via analysis of possible utility bounds","volume-title":"Proc. ICSE","author":"Stevens","year":"2020"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-016-0360-8"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2013.6606683"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1145\/3236024.3275534"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2013.15"},{"key":"ref11","first-page":"61","article-title":"Synthesis of assurance cases for software certification","volume-title":"Proc. 42nd Int. Conf. Softw. Eng., New Ideas Emerg. Results (ICSE-NIER)","author":"Bagheri","year":"2020"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1145\/2001420.2001429"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1145\/2483760.2483770"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1145\/2642937.2643012"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129512000291"},{"key":"ref16","first-page":"1","article-title":"The margrave tool for firewall analysis","volume-title":"Proc. Uncovering Secrets Syst. Admin.: Proc. 24th Large Installation Syst. Admin. Conf.","author":"Nelson","year":"2010"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1145\/2534169.2491711"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-43652-3_31"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1109\/DSN.2016.53"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-19249-9_6"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1007\/s10664-020-09932-6"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-48992-6_21"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1145\/3395363.3397347"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1145\/2950290.2950336"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1023\/B:AUSE.0000038938.10589.b9"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1145\/2884781.2884853"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1145\/1512762.1512764"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2001.989787"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1109\/formalise58978.2023.00013"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE-Companion.2019.00049"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1145\/3533767.3534369"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1109\/ICSME46990.2020.00107"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1145\/3551349.3556944"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE43902.2021.00105"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1109\/ASE51524.2021.9678524"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-77382-2_18"},{"key":"ref37","first-page":"1877","article-title":"Language models are few-shot learners","volume-title":"Proc. Adv. Neural Inf. Process. Syst.","volume":"33","author":"Brown","year":"2020"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.48550\/ARXIV.1706.03762"},{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1145\/3520312.3534862"},{"key":"ref40","article-title":"Gemini: A family of highly capable multimodal models","author":"Team","year":"2023"},{"key":"ref41","article-title":"Experiences on teaching Alloy with an automated assessment platform","volume-title":"Sci. Computer Program.","volume":"211","author":"Macedo","year":"2021"},{"key":"ref42","article-title":"Automated repair of Alloy specifications in the era of large language models","author":"Hasan","year":"2025"},{"key":"ref43","doi-asserted-by":"publisher","DOI":"10.52202\/068431-1613"},{"key":"ref44","doi-asserted-by":"publisher","DOI":"10.18653\/v1\/2021.findings-emnlp.244"},{"key":"ref45","doi-asserted-by":"publisher","DOI":"10.18653\/v1\/2022.emnlp-main.801"},{"key":"ref46","article-title":"Role-playing prompt framework: Generation and evaluation","author":"Liu","year":"2024"},{"key":"ref47","doi-asserted-by":"publisher","DOI":"10.1145\/3238147.3238162"},{"key":"ref48","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.10.001"},{"key":"ref49","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2013.6606623"},{"key":"ref50","doi-asserted-by":"publisher","DOI":"10.1145\/2884781.2884807"},{"key":"ref51","doi-asserted-by":"publisher","DOI":"10.1145\/1993316.1993544"},{"key":"ref52","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2011.104"},{"key":"ref53","doi-asserted-by":"publisher","DOI":"10.1145\/2914770.2837617"},{"key":"ref54","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2013.6606626"},{"key":"ref55","doi-asserted-by":"crossref","first-page":"602","DOI":"10.1145\/3377811.3380345","article-title":"DLFix: Context-based code transformation learning for automated program repair","volume-title":"Proc. ACM\/IEEE 42nd Int. Conf. Softw. Eng. (ICSE)","author":"Li","year":"2020"},{"key":"ref56","doi-asserted-by":"publisher","DOI":"10.1007\/s10664-019-09780-z"},{"key":"ref57","doi-asserted-by":"publisher","DOI":"10.1145\/3338906.3340455"},{"key":"ref58","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-012-0249-7"},{"key":"ref59","article-title":"ExCAPE Project: Expeditions in computer augmented program engineering","year":"2020"},{"key":"ref60","article-title":"Sygus","year":"2020"},{"key":"ref61","doi-asserted-by":"publisher","DOI":"10.1109\/ICST.2018.00047"},{"key":"ref62","doi-asserted-by":"publisher","DOI":"10.1109\/ISSRE5003.2020.00044"},{"key":"ref63","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE43902.2021.00065"},{"key":"ref64","article-title":"Evaluating large language models trained on code","author":"Chen","year":"2021"},{"key":"ref65","doi-asserted-by":"publisher","DOI":"10.1145\/3650212.3680323"},{"key":"ref66","article-title":"Z: An introduction to formal methods","author":"Antoni","year":"1990"},{"key":"ref67","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48153-2_6"},{"key":"ref68","volume-title":"Systematic Software Development Using VDM.","author":"Jones","year":"1986"}],"container-title":["IEEE Transactions on Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx8\/32\/11613940\/11478669.pdf?arnumber=11478669","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,18]],"date-time":"2026-07-18T05:26:32Z","timestamp":1784352392000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/11478669\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,7]]},"references-count":68,"journal-issue":{"issue":"7"},"URL":"https:\/\/doi.org\/10.1109\/tse.2026.3682711","relation":{},"ISSN":["0098-5589","1939-3520","2326-3881"],"issn-type":[{"value":"0098-5589","type":"print"},{"value":"1939-3520","type":"electronic"},{"value":"2326-3881","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,7]]}}}