{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,21]],"date-time":"2026-07-21T17:07:15Z","timestamp":1784653635388,"version":"3.55.0"},"publisher-location":"New York, NY, USA","reference-count":43,"publisher":"ACM","license":[{"start":{"date-parts":[[2026,4,12]],"date-time":"2026-04-12T00:00:00Z","timestamp":1775952000000},"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":[],"published-print":{"date-parts":[[2026,4,12]]},"DOI":"10.1145\/3793655.3793731","type":"proceedings-article","created":{"date-parts":[[2026,7,21]],"date-time":"2026-07-21T16:04:46Z","timestamp":1784649886000},"page":"29-39","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["AutoReSpec: A Framework for Generating Specification using Large Language Models"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0006-6372-5000","authenticated-orcid":false,"given":"Ragib Shahariar","family":"Ayon","sequence":"first","affiliation":[{"name":"Department of Computer Science, Texas State University, San Marcos, TX, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1183-883X","authenticated-orcid":false,"given":"Shibbir","family":"Ahmed","sequence":"additional","affiliation":[{"name":"Department of Computer Science, Texas State University, San Marcos, TX, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,7,21]]},"reference":[{"key":"e_1_3_3_1_2_2","unstructured":"2025. OpenJML 21-0.8. https:\/\/github.com\/OpenJML\/OpenJML\/releases\/tag\/21-0.8. [Online; accessed Oct-2025]."},{"key":"e_1_3_3_1_3_2","unstructured":"2025. OpenJML Repository. https:\/\/github.com\/OpenJML\/OpenJML\/tree\/master-21. [Online; accessed Oct-2025]."},{"key":"e_1_3_3_1_4_2","doi-asserted-by":"crossref","unstructured":"Parosh\u00a0Aziz Abdulla and Bengt Jonsson. 1996. Undecidable verification problems for programs with unreliable channels. Information and Computation 130 1 (1996) 71\u201390.","DOI":"10.1006\/inco.1996.0083"},{"key":"e_1_3_3_1_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/3551349.3559555"},{"key":"e_1_3_3_1_6_2","doi-asserted-by":"crossref","unstructured":"Wolfgang Ahrendt Thomas Baar Bernhard Beckert Richard Bubel Martin Giese Reiner H\u00e4hnle Wolfram Menzel Wojciech Mostowski Andreas Roth Steffen Schlager et\u00a0al. 2005. The KeY tool: integrating object oriented design and formal verification. Software & Systems Modeling 4 (2005) 32\u201354.","DOI":"10.1007\/s10270-004-0058-x"},{"key":"e_1_3_3_1_7_2","doi-asserted-by":"crossref","unstructured":"Anoud Alshnakat Dilian Gurov Christian Lidstr\u00f6m and Philipp R\u00fcmmer. 2020. Constraint-based contract inference for deductive verification. Deductive Software Verification: Future Perspectives: Reflections on the Occasion of 20 Years of KeY (2020) 149\u2013176.","DOI":"10.1007\/978-3-030-64354-6_6"},{"key":"e_1_3_3_1_8_2","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"e_1_3_3_1_9_2","unstructured":"Ragib\u00a0Shahariar Ayon. 2025. AutoReSpec Algorithm Notation. https:\/\/github.com\/autorespec\/AutoReSpec\/blob\/main\/Algorithm\/Algorithm%20Notation.png. [Online; accessed Nov-2025]."},{"key":"e_1_3_3_1_10_2","unstructured":"Ragib\u00a0Shahariar Ayon. 2025. AutoReSpec Leaderboard. https:\/\/autorespec.github.io\/AutoReSpecLeaderboard\/. [Online; accessed Nov-2025]."},{"key":"e_1_3_3_1_11_2","unstructured":"Ragib\u00a0Shahariar Ayon. 2025. AutoReSpec Prompts. https:\/\/github.com\/autorespec\/AutoReSpec\/tree\/main\/Prompts. [Online; accessed Nov-2025]."},{"key":"e_1_3_3_1_12_2","unstructured":"Ragib\u00a0Shahariar Ayon. 2025. AutoReSpec Replication Package. https:\/\/github.com\/autorespec\/AutoReSpec\/tree\/main\/Leaderboard. [Online; accessed Nov-2025]."},{"key":"e_1_3_3_1_13_2","unstructured":"Ragib\u00a0Shahariar Ayon. 2025. AutoReSpec Repository. https:\/\/github.com\/autorespec\/AutoReSpec. [Online; accessed Nov-2025]."},{"key":"e_1_3_3_1_14_2","unstructured":"Ragib\u00a0Shahariar Ayon. 2025. AutoReSpec VS Code Extension. https:\/\/github.com\/autorespec\/AutoReSpec\/tree\/main\/VS-Code%20Extension. [Online; accessed Nov-2025]."},{"key":"e_1_3_3_1_15_2","unstructured":"Tom Brown Benjamin Mann Nick Ryder Melanie Subbiah Jared\u00a0D Kaplan Prafulla Dhariwal Arvind Neelakantan Pranav Shyam Girish Sastry Amanda Askell et\u00a0al. 2020. Language models are few-shot learners. Advances in neural information processing systems 33 (2020) 1877\u20131901."},{"key":"e_1_3_3_1_16_2","doi-asserted-by":"crossref","unstructured":"Saikat Chakraborty Shuvendu\u00a0K Lahiri Sarah Fakhoury Madanlal Musuvathi Akash Lal Aseem Rastogi Aditya Senthilnathan Rahul Sharma and Nikhil Swamy. 2023. Ranking llm-generated loop invariants for program verification. arXiv preprint arXiv:https:\/\/arXiv.org\/abs\/2310.09342 (2023).","DOI":"10.18653\/v1\/2023.findings-emnlp.614"},{"key":"e_1_3_3_1_17_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35873-9_10"},{"key":"e_1_3_3_1_18_2","doi-asserted-by":"crossref","unstructured":"Michael\u00a0D Ernst Jeff\u00a0H Perkins Philip\u00a0J Guo Stephen McCamant Carlos Pacheco Matthew\u00a0S Tschantz and Chen Xiao. 2007. The Daikon system for dynamic detection of likely invariants. Science of computer programming 69 1-3 (2007) 35\u201345.","DOI":"10.1016\/j.scico.2007.01.015"},{"key":"e_1_3_3_1_19_2","doi-asserted-by":"publisher","unstructured":"Cormac Flanagan Gary Leavens K.\u00a0Rustan\u00a0M. Leino and Erik Poll. 2002. JML: Notation for Detailed Design. In Behavioral Specifications of Businesses and Systems (2002) 175\u2013188. 10.1007\/978-1-4615-0881-8_12","DOI":"10.1007\/978-1-4615-0881-8_12"},{"key":"e_1_3_3_1_20_2","doi-asserted-by":"publisher","DOI":"10.5555\/647540.730008"},{"key":"e_1_3_3_1_21_2","doi-asserted-by":"crossref","unstructured":"Xinyi Hou Yanjie Zhao Yue Liu Zhou Yang Kailong Wang Li Li Xiapu Luo David Lo John Grundy and Haoyu Wang. 2024. Large language models for software engineering: A systematic literature review. ACM Transactions on Software Engineering and Methodology 33 8 (2024) 1\u201379.","DOI":"10.1145\/3695988"},{"key":"e_1_3_3_1_22_2","doi-asserted-by":"publisher","DOI":"10.18653\/v1\/2023.findings-emnlp.123"},{"key":"e_1_3_3_1_23_2","doi-asserted-by":"publisher","DOI":"10.1145\/2610384.2628053"},{"key":"e_1_3_3_1_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/3650212.3680310"},{"key":"e_1_3_3_1_25_2","doi-asserted-by":"crossref","unstructured":"Thanh Le-Cong Bach Le and Toby Murray. 2025. Can LLMs Reason About Program Semantics? A Comprehensive Evaluation of LLMs on Formal Specification Inference. (2025). https:\/\/openreview.net\/forum?id=zXyiakJYzB","DOI":"10.18653\/v1\/2025.acl-long.1068"},{"key":"e_1_3_3_1_26_2","unstructured":"Thanh Le-Cong Bach Le and Toby Murray. 2025. Can LLMs Reason About Program Semantics? A Comprehensive Evaluation of LLMs on Formal Specification Inference. arXiv preprint arXiv:https:\/\/arXiv.org\/abs\/2503.04779 (2025)."},{"key":"e_1_3_3_1_27_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31145-5_12"},{"key":"e_1_3_3_1_28_2","doi-asserted-by":"publisher","DOI":"10.1145\/3466752.3480125"},{"key":"e_1_3_3_1_29_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE55347.2025.00129"},{"key":"e_1_3_3_1_30_2","first-page":"158","volume-title":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","author":"Mathur Umang","year":"2020","unstructured":"Umang Mathur, P Madhusudan, and Mahesh Viswanathan. 2020. What\u2019s decidable about program verification modulo axioms?. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 158\u2013177."},{"key":"e_1_3_3_1_31_2","doi-asserted-by":"crossref","unstructured":"Quinn McNemar. 1947. Note on the sampling error of the difference between correlated proportions or percentages. Psychometrika 12 2 (1947) 153\u2013157.","DOI":"10.1007\/BF02295996"},{"key":"e_1_3_3_1_32_2","doi-asserted-by":"publisher","unstructured":"Md\u00a0Rakib\u00a0Hossain Misu Cristina\u00a0V. Lopes Iris Ma and James Noble. 2024. Towards AI-Assisted Synthesis of Verified Dafny Methods. Proc. ACM Softw. Eng. 1 FSE Article 37 (July 2024) 24\u00a0pages. 10.1145\/3643763","DOI":"10.1145\/3643763"},{"key":"e_1_3_3_1_33_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE43902.2021.00112"},{"key":"e_1_3_3_1_34_2","doi-asserted-by":"crossref","unstructured":"Long Ouyang Jeffrey Wu Xu Jiang Diogo Almeida Carroll Wainwright Pamela Mishkin Chong Zhang Sandhini Agarwal Katarina Slama Alex Ray et\u00a0al. 2022. Training language models to follow instructions with human feedback. Advances in neural information processing systems 35 (2022) 27730\u201327744.","DOI":"10.52202\/068431-2011"},{"key":"e_1_3_3_1_35_2","first-page":"27496","volume-title":"International Conference on Machine Learning","author":"Pei Kexin","year":"2023","unstructured":"Kexin Pei, David Bieber, Kensen Shi, Charles Sutton, and Pengcheng Yin. 2023. Can large language models reason about program invariants?. In International Conference on Machine Learning. PMLR, 27496\u201327520."},{"key":"e_1_3_3_1_36_2","unstructured":"sosy lab. 2024. SV-COMP - International Competition on Software Verification. https:\/\/sites.google.com\/view\/specgen."},{"key":"e_1_3_3_1_37_2","unstructured":"Xinchen Wang Pengfei Gao Chao Peng Ruida Hu and Cuiyun Gao. 2025. CodeVisionary: An Agent-based Framework for Evaluating Large Language Models in Code Generation. arxiv:https:\/\/arXiv.org\/abs\/2504.13472\u00a0[cs.SE] https:\/\/arxiv.org\/abs\/2504.13472"},{"key":"e_1_3_3_1_38_2","doi-asserted-by":"crossref","unstructured":"Cheng Wen Jialun Cao Jie Su Zhiwu Xu Shengchao Qin Mengda He Haokun Li Shing-Chi Cheung and Cong Tian. 2024. Enchanting program specification synthesis by large language models using static analysis and program verification. arXiv preprint arXiv:https:\/\/arXiv.org\/abs\/2404.00762 (2024).","DOI":"10.1007\/978-3-031-65630-9_16"},{"key":"e_1_3_3_1_39_2","doi-asserted-by":"crossref","unstructured":"Frank Wilcoxon. 1945. Individual comparisons by ranking methods. Biometrics bulletin 1 6 (1945) 80\u201383.","DOI":"10.2307\/3001968"},{"key":"e_1_3_3_1_40_2","unstructured":"Qinyun Wu Chao Peng Pengfei Gao Ruida Hu Haoyu Gan Bo Jiang Jinhe Tang Zhiwen Deng Zhanming Guan Cuiyun Gao et\u00a0al. 2024. Repomastereval: Evaluating code completion via real-world repositories. arXiv preprint arXiv:https:\/\/arXiv.org\/abs\/2408.03519 (2024)."},{"key":"e_1_3_3_1_41_2","doi-asserted-by":"publisher","DOI":"10.1145\/3650212.3680323"},{"key":"e_1_3_3_1_42_2","doi-asserted-by":"crossref","unstructured":"Xiaofei Xie Bihuan Chen Liang Zou Yang Liu Wei Le and Xiaohong Li. 2017. Automatic loop summarization via path dependency analysis. IEEE Transactions on Software Engineering 45 6 (2017) 537\u2013557.","DOI":"10.1109\/TSE.2017.2788018"},{"key":"e_1_3_3_1_43_2","doi-asserted-by":"publisher","DOI":"10.1145\/3533767.3534390"},{"key":"e_1_3_3_1_44_2","unstructured":"Yue Zhang Yafu Li Leyang Cui Deng Cai Lemao Liu Tingchen Fu Xinting Huang Enbo Zhao Yu Zhang Yulong Chen et\u00a0al. 2023. Siren\u2019s song in the AI ocean: a survey on hallucination in large language models. arXiv preprint arXiv:https:\/\/arXiv.org\/abs\/2309.01219 (2023)."}],"event":{"name":"FORGE '26: IEEE\/ACM Third International Conference on AI Foundation Models and Software Engineering","location":"Rio de Janeiro , Brazil","acronym":"FORGE '26","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering"]},"container-title":["Proceedings of the 2026 IEEE\/ACM Third International Conference on AI Foundation Models and Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3793655.3793731","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,21]],"date-time":"2026-07-21T16:49:32Z","timestamp":1784652572000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3793655.3793731"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,4,12]]},"references-count":43,"alternative-id":["10.1145\/3793655.3793731","10.1145\/3793655"],"URL":"https:\/\/doi.org\/10.1145\/3793655.3793731","relation":{},"subject":[],"published":{"date-parts":[[2026,4,12]]},"assertion":[{"value":"2026-07-21","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}