{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,19]],"date-time":"2026-03-19T21:47:24Z","timestamp":1773956844705,"version":"3.50.1"},"reference-count":62,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2026,2,1]],"date-time":"2026-02-01T00:00:00Z","timestamp":1769904000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2026,2,1]],"date-time":"2026-02-01T00:00:00Z","timestamp":1769904000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"},{"start":{"date-parts":[[2026,2,1]],"date-time":"2026-02-01T00:00:00Z","timestamp":1769904000000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-017"},{"start":{"date-parts":[[2026,2,1]],"date-time":"2026-02-01T00:00:00Z","timestamp":1769904000000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"},{"start":{"date-parts":[[2026,2,1]],"date-time":"2026-02-01T00:00:00Z","timestamp":1769904000000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-012"},{"start":{"date-parts":[[2026,2,1]],"date-time":"2026-02-01T00:00:00Z","timestamp":1769904000000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2026,2,1]],"date-time":"2026-02-01T00:00:00Z","timestamp":1769904000000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-004"}],"funder":[{"DOI":"10.13039\/100012897","name":"ZTE Corporation","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100012897","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["62432007"],"award-info":[{"award-number":["62432007"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["62272165"],"award-info":[{"award-number":["62272165"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["62441605"],"award-info":[{"award-number":["62441605"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Knowledge-Based Systems"],"published-print":{"date-parts":[[2026,2]]},"DOI":"10.1016\/j.knosys.2025.115177","type":"journal-article","created":{"date-parts":[[2025,12,24]],"date-time":"2025-12-24T00:12:34Z","timestamp":1766535154000},"page":"115177","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":0,"special_numbering":"C","title":["NL2ACSL : Interactively translating natural language to ANSI C specification language with large language models"],"prefix":"10.1016","volume":"335","author":[{"ORCID":"https:\/\/orcid.org\/0009-0008-2470-8843","authenticated-orcid":false,"given":"Wenxian","family":"Su","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5795-9798","authenticated-orcid":false,"given":"Xi","family":"Wu","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9561-7403","authenticated-orcid":false,"given":"Yongxin","family":"Zhao","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"issue":"1","key":"10.1016\/j.knosys.2025.115177_bib0001","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1109\/TSE.2011.28","article-title":"Invariant-based automatic testing of modern web applications","volume":"38","author":"Mesbah","year":"2011","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"06","key":"10.1016\/j.knosys.2025.115177_bib0002","doi-asserted-by":"crossref","first-page":"953","DOI":"10.1142\/S0218194023500225","article-title":"TC4MT: a specification-driven testing framework for model transformations","volume":"33","author":"Nguyen","year":"2023","journal-title":"Int. J. Softw. Eng. Knowl. Eng."},{"key":"10.1016\/j.knosys.2025.115177_bib0003","first-page":"79","article-title":"ACSL: ansi C specification language","volume":"2","author":"Baudin","year":"2008","journal-title":"CEA-LIST, Saclay, France, Tech. Rep. v1"},{"key":"10.1016\/j.knosys.2025.115177_bib0004","unstructured":"J. Burghardt, J. Gerlach, K. Hartig, H. Pohl, J. Soto, ACSL by example, DEVICE-SOFT project publication. Fraunhofer FIRST Institute (2010)."},{"key":"10.1016\/j.knosys.2025.115177_bib0005","series-title":"AIP Conference Proceedings","doi-asserted-by":"crossref","first-page":"020010","DOI":"10.1063\/5.0153960","article-title":"Natural language processing: a review","volume":"2771","author":"Gangal","year":"2023"},{"key":"10.1016\/j.knosys.2025.115177_bib0006","series-title":"2021 IEEE 8th Uttar Pradesh Section International Conference on Electrical, Electronics and Computer Engineering (UPCON)","first-page":"1","article-title":"A review of neural machine translation based on deep learning techniques","author":"Sharma","year":"2021"},{"issue":"7","key":"10.1016\/j.knosys.2025.115177_bib0007","doi-asserted-by":"crossref","first-page":"1716","DOI":"10.3390\/electronics12071716","article-title":"Machine translation systems based on classical-statistical-deep-learning approaches","volume":"12","author":"Sharma","year":"2023","journal-title":"Electronics"},{"key":"10.1016\/j.knosys.2025.115177_bib0008","series-title":"2023 3rd International Conference on Innovative Sustainable Computational Technologies (CISCT)","first-page":"1","article-title":"Unlocking the power of natural language processing through journaling with the assistance","author":"Mishra","year":"2023"},{"key":"10.1016\/j.knosys.2025.115177_bib0009","series-title":"Distributed Computing and Optimization Techniques: Select Proceedings of ICDCOT 2021","first-page":"593","article-title":"Machine translation for indian languages utilizing recurrent neural networks and attention","author":"Sharma","year":"2022"},{"key":"10.1016\/j.knosys.2025.115177_bib0010","series-title":"2025 International Conference on Intelligent Control, Computing and Communications (IC3)","first-page":"458","article-title":"Deep learning-based sign language recognition: a comprehensive analysis","author":"Tyagi","year":"2025"},{"issue":"2","key":"10.1016\/j.knosys.2025.115177_bib0011","first-page":"50","article-title":"Network architecture and technologies for generative models","volume":"30","author":"TANG","year":"2024","journal-title":"ZTE Technol. J."},{"issue":"2","key":"10.1016\/j.knosys.2025.115177_bib0012","first-page":"76","article-title":"Key technologies and applications of large models","volume":"30","author":"HAN","year":"2024","journal-title":"ZTE Technol. J."},{"issue":"8","key":"10.1016\/j.knosys.2025.115177_bib0013","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3695988","article-title":"Large language models for software engineering: a systematic literature review","volume":"33","author":"Hou","year":"2024","journal-title":"ACM Trans. Softw. Eng. Method."},{"key":"10.1016\/j.knosys.2025.115177_bib0014","unstructured":"C.S. Xia, L. Zhang, Conversational automated program repair, arXiv preprint arXiv: 2301.13246(2023)."},{"key":"10.1016\/j.knosys.2025.115177_bib0015","unstructured":"M. Chen, Evaluating large language models trained on code, arXiv preprint arXiv: 2107.03374(2021)."},{"key":"10.1016\/j.knosys.2025.115177_bib0016","series-title":"International Conference on Computer Aided Verification","first-page":"302","article-title":"Enchanting program specification synthesis by large language models using static analysis and program verification","author":"Wen","year":"2024"},{"key":"10.1016\/j.knosys.2025.115177_bib0017","unstructured":"L. Ma, S. Liu, Y. Li, X. Xie, L. Bu, SpecGen: automated generation of formal program specifications via large language models, arXiv preprint arXiv: 2401.08807(2024)."},{"key":"10.1016\/j.knosys.2025.115177_bib0018","series-title":"International Conference on Computer Aided Verification","first-page":"383","article-title":"nl2spec: interactively translating unstructured natural language to temporal logics with large language models","author":"Cosler","year":"2023"},{"key":"10.1016\/j.knosys.2025.115177_bib0019","series-title":"Proceedings of the 30th Asia and South Pacific Design Automation Conference","first-page":"614","article-title":"AssertLLM: generating hardware verification assertions from design specifications via multi-LLMs","author":"Yan","year":"2025"},{"key":"10.1016\/j.knosys.2025.115177_bib0020","series-title":"Proceedings of the 63rd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers)","first-page":"26984","article-title":"From informal to formal \u2013 incorporating and evaluating LLMs on natural language requirements to verifiable formal proofs","author":"Cao","year":"2025"},{"key":"10.1016\/j.knosys.2025.115177_bib0021","first-page":"9459","article-title":"Retrieval-augmented generation for knowledge-intensive NLP tasks","volume":"33","author":"Lewis","year":"2020","journal-title":"Adv. Neural Inf. Process. Syst."},{"key":"10.1016\/j.knosys.2025.115177_bib0022","unstructured":"J. Achiam, S. Adler, S. Agarwal, L. Ahmad, I. Akkaya, F.L. Aleman, D. Almeida, J. Altenschmidt, S. Altman, S. Anadkat, et al., GPT-4 technical report, arXiv preprint arXiv: 2303.08774(2023)."},{"key":"10.1016\/j.knosys.2025.115177_bib0023","unstructured":"A. Liu, B. Feng, B. Xue, B. Wang, B. Wu, C. Lu, C. Zhao, C. Deng, C. Zhang, C. Ruan, et al., DeepSeek-V3 technical report, arXiv preprint arXiv: 2412.19437(2024)."},{"issue":"3","key":"10.1016\/j.knosys.2025.115177_bib0024","doi-asserted-by":"crossref","first-page":"573","DOI":"10.1007\/s00165-014-0326-7","article-title":"Frama-C: a software analysis perspective","volume":"27","author":"Kirchner","year":"2015","journal-title":"Formal Aspects Comput."},{"key":"10.1016\/j.knosys.2025.115177_bib0025","first-page":"33","article-title":"A refinement of the extended euclidean algorithm","volume":"15","author":"Iliev","year":"2021","journal-title":"Int. Electr. J. Pure Appl. Math."},{"key":"10.1016\/j.knosys.2025.115177_bib0026","unstructured":"J. Jiang, F. Wang, J. Shen, S. Kim, S. Kim, A survey on large language models for code generation, arXiv preprint arXiv: 2406.00515(2024)."},{"key":"10.1016\/j.knosys.2025.115177_bib0027","unstructured":"J. Ye, X. Chen, N. Xu, C. Zu, Z. Shao, S. Liu, Y. Cui, Z. Zhou, C. Gong, Y. Shen, et al., A comprehensive capability analysis of GPT-3 and GPT-3.5 series models, arXiv preprint arXiv: 2303.10420(2023)."},{"key":"10.1016\/j.knosys.2025.115177_bib0028","series-title":"Proceedings of the 54th ACM Technical Symposium on Computer Science Education V. 1","first-page":"172","article-title":"Using GitHub copilot to solve simple programming problems","author":"Wermelinger","year":"2023"},{"key":"10.1016\/j.knosys.2025.115177_bib0029","doi-asserted-by":"crossref","first-page":"28573","DOI":"10.1109\/ACCESS.2018.2831228","article-title":"Multi-agent systems: a survey","volume":"6","author":"Dorri","year":"2018","journal-title":"IEEE Access"},{"key":"10.1016\/j.knosys.2025.115177_bib0030","unstructured":"T. Guo, X. Chen, Y. Wang, R. Chang, S. Pei, N.V. Chawla, O. Wiest, X. Zhang, Large language model based multi-agents: a survey of progress and challenges, arXiv preprint arXiv: 2402.01680(2024)."},{"key":"10.1016\/j.knosys.2025.115177_bib0031","doi-asserted-by":"crossref","first-page":"3781","DOI":"10.1016\/j.procs.2024.09.178","article-title":"A survey on RAG with LLMs","volume":"246","author":"Arslan","year":"2024","journal-title":"Procedia Comput. Sci."},{"key":"10.1016\/j.knosys.2025.115177_bib0032","unstructured":"D. Edge, H. Trinh, N. Cheng, J. Bradley, A. Chao, A. Mody, S. Truitt, D. Metropolitansky, R.O. Ness, J. Larson, From local to global: a graph rag approach to query-focused summarization, arXiv preprint arXiv: 2404.16130(2024)."},{"issue":"9","key":"10.1016\/j.knosys.2025.115177_bib0033","first-page":"1","article-title":"Pre-train, prompt, and predict: a systematic survey of prompting methods in natural language processing","volume":"55","author":"Liu","year":"2023","journal-title":"ACM Comput. Surv."},{"key":"10.1016\/j.knosys.2025.115177_bib0034","unstructured":"S. Schulhoff, M. Ilie, N. Balepur, K. Kahadze, A. Liu, C. Si, Y. Li, A. Gupta, H. Han, S. Schulhoff, et al., The prompt report: a systematic survey of prompt engineering techniques, arXiv preprint arXiv: 2406.06608(2024)."},{"key":"10.1016\/j.knosys.2025.115177_bib0035","first-page":"24824","article-title":"Chain-of-thought prompting elicits reasoning in large language models","volume":"35","author":"Wei","year":"2022","journal-title":"Adv. Neural Inf. Process. Syst."},{"key":"10.1016\/j.knosys.2025.115177_bib0036","unstructured":"X. Wang, J. Wei, D. Schuurmans, Q. Le, E. Chi, S. Narang, A. Chowdhery, D. Zhou, Self-consistency improves chain of thought reasoning in language models, arXiv preprint arXiv: 2203.11171(2022)."},{"key":"10.1016\/j.knosys.2025.115177_bib0037","series-title":"2025 IEEE International Conference on Robotics and Automation (ICRA)","first-page":"9011","article-title":"ExplorLLM: guiding exploration in reinforcement learning with large language models","author":"Ma","year":"2025"},{"key":"10.1016\/j.knosys.2025.115177_bib0038","unstructured":"H. Zhong, Z. Shan, G. Feng, W. Xiong, X. Cheng, L. Zhao, D. He, J. Bian, L. Wang, DPO meets PPO: Reinforced token optimization for RLHF, arXiv preprint arXiv: 2404.18922(2024)."},{"key":"10.1016\/j.knosys.2025.115177_bib0039","unstructured":"H. Dong, W. Xiong, B. Pang, H. Wang, H. Zhao, Y. Zhou, N. Jiang, D. Sahoo, C. Xiong, T. Zhang, RLHF workflow: from reward modeling to online RLHF, arXiv preprint arXiv: 2405.07863(2024)."},{"key":"10.1016\/j.knosys.2025.115177_bib0040","unstructured":"H. Han, J. Kim, J. Yoo, Y. Lee, S.-w. Hwang, ArchCode: incorporating software requirements in code generation with large language models, arXiv preprint arXiv: 2408.00994(2024)."},{"key":"10.1016\/j.knosys.2025.115177_bib0041","first-page":"65030","article-title":"Grammar prompting for domain-specific language generation with large language models","volume":"36","author":"Wang","year":"2023","journal-title":"Adv. Neural Inf. Process. Syst."},{"key":"10.1016\/j.knosys.2025.115177_bib0042","unstructured":"Z. Guo, L. Xia, Y. Yu, T. Ao, C. Huang, LightRAG: simple and fast retrieval-augmented generation, arXiv preprint arXiv: 2410.05779(2024)."},{"key":"10.1016\/j.knosys.2025.115177_bib0043","unstructured":"W. Xiong, H. Dong, C. Ye, Z. Wang, H. Zhong, H. Ji, N. Jiang, T. Zhang, Iterative preference learning from human feedback: bridging theory and practice for RLHF under KL-constraint, arXiv preprint arXiv: 2312.11456(2023)."},{"key":"10.1016\/j.knosys.2025.115177_bib0044","doi-asserted-by":"crossref","unstructured":"H. Wang, W. Xiong, T. Xie, H. Zhao, T. Zhang, Interpretable preferences via multi-objective reward modeling and mixture-of-experts, arXiv preprint arXiv: 2406.12845(2024).","DOI":"10.18653\/v1\/2024.findings-emnlp.620"},{"key":"10.1016\/j.knosys.2025.115177_bib0045","unstructured":"A. Dubey, A. Jauhri, A. Pandey, A. Kadian, A. Al-Dahle, A. Letman, A. Mathur, A. Schelten, A. Yang, A. Fan, et al., The Llama 3 herd of models, arXiv e-prints (2024) arXiv\u20132407."},{"issue":"1","key":"10.1016\/j.knosys.2025.115177_bib0046","article-title":"Generalized Bradley-Terry models and multi-class probability estimates","volume":"7","author":"Huang","year":"2006","journal-title":"J. Mach. Learn. Res."},{"key":"10.1016\/j.knosys.2025.115177_bib0047","series-title":"2025 IEEE\/ACM 22nd International Conference on Mining Software Repositories (MSR)","first-page":"758","article-title":"FormalSpecCpp: a dataset of C++ formal specifications created using LLMs","author":"Chakraborty","year":"2025"},{"key":"10.1016\/j.knosys.2025.115177_bib0048","unstructured":"M. Patnaik, N. Karthikeyan, Frama-C problems repository, 2025, (https:\/\/github.com\/manavpatnaik\/frama-c-problems). Accessed: 10 July 2025."},{"key":"10.1016\/j.knosys.2025.115177_bib0049","unstructured":"N. Hertzberg, CASP_dataset, 2025, (https:\/\/huggingface.co\/datasets\/nicher92\/CASP_dataset). Accessed: 23 October 2025."},{"key":"10.1016\/j.knosys.2025.115177_bib0050","first-page":"22199","article-title":"Large language models are zero-shot reasoners","volume":"35","author":"Kojima","year":"2022","journal-title":"Adv. Neural Inf. Process. Syst."},{"key":"10.1016\/j.knosys.2025.115177_bib0051","series-title":"Extended Abstracts of the 2021 CHI Conference on Human Factors in Computing Systems","first-page":"1","article-title":"Prompt programming for large language models: beyond the few-shot paradigm","author":"Reynolds","year":"2021"},{"issue":"1","key":"10.1016\/j.knosys.2025.115177_bib0052","doi-asserted-by":"crossref","first-page":"250","DOI":"10.1049\/cit2.12207","article-title":"DeepOCL: a deep neural network for object constraint language generation from unrestricted nature language","volume":"9","author":"Yang","year":"2024","journal-title":"CAAI Trans. Intell. Technol."},{"key":"10.1016\/j.knosys.2025.115177_bib0053","series-title":"Proceedings of the 40th Annual Meeting of the Association for Computational Linguistics","first-page":"311","article-title":"Bleu: a method for automatic evaluation of machine translation","author":"Papineni","year":"2002"},{"key":"10.1016\/j.knosys.2025.115177_bib0054","series-title":"Text Summarization Branches Out","first-page":"74","article-title":"Rouge: a package for automatic evaluation of summaries","author":"Lin","year":"2004"},{"key":"10.1016\/j.knosys.2025.115177_bib0055","series-title":"International Symposium on AI Verification","first-page":"134","article-title":"Clover: clo sed-loop ver ifiable code generation","author":"Sun","year":"2024"},{"key":"10.1016\/j.knosys.2025.115177_bib0056","series-title":"Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering","first-page":"1229","article-title":"Baldur: whole-proof generation and repair with large language models","author":"First","year":"2023"},{"key":"10.1016\/j.knosys.2025.115177_bib0057","series-title":"Proceedings of the IEEE\/ACM 47th International Conference on Software Engineering","first-page":"307","article-title":"QEDCartographer: automating formal verification using reward-free reinforcement learning","author":"Sanchez-Stern","year":"2025"},{"issue":"FSE","key":"10.1016\/j.knosys.2025.115177_bib0058","doi-asserted-by":"crossref","first-page":"812","DOI":"10.1145\/3643763","article-title":"Towards AI-assisted synthesis of verified dafny methods","volume":"1","author":"Misu","year":"2024","journal-title":"Proc. ACM Softw. Eng."},{"key":"10.1016\/j.knosys.2025.115177_bib0059","series-title":"2023 53rd Annual IEEE\/IFIP International Conference on Dependable Systems and Networks Workshops (DSN-W)","first-page":"259","article-title":"Translating natural language requirements to formal specifications: a study on GPT and symbolic NLP","author":"Leong","year":"2023"},{"key":"10.1016\/j.knosys.2025.115177_bib0060","series-title":"International Conference on Integrated Formal Methods","first-page":"307","article-title":"Specify what? Enhancing neural specification synthesis by symbolic methods","author":"Granberry","year":"2024"},{"key":"10.1016\/j.knosys.2025.115177_bib0061","series-title":"International Symposium of Formal Methods Europe","first-page":"500","article-title":"Houdini, an annotation assistant for ESC\/Java","author":"Flanagan","year":"2001"},{"issue":"1-3","key":"10.1016\/j.knosys.2025.115177_bib0062","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1016\/j.scico.2007.01.015","article-title":"The Daikon system for dynamic detection of likely invariants","volume":"69","author":"Ernst","year":"2007","journal-title":"Sci. Comput. Program."}],"container-title":["Knowledge-Based Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0950705125022117?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0950705125022117?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2026,3,19]],"date-time":"2026-03-19T17:37:10Z","timestamp":1773941830000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0950705125022117"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,2]]},"references-count":62,"alternative-id":["S0950705125022117"],"URL":"https:\/\/doi.org\/10.1016\/j.knosys.2025.115177","relation":{},"ISSN":["0950-7051"],"issn-type":[{"value":"0950-7051","type":"print"}],"subject":[],"published":{"date-parts":[[2026,2]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"NL2ACSL : Interactively translating natural language to ANSI C specification language with large language models","name":"articletitle","label":"Article Title"},{"value":"Knowledge-Based Systems","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/j.knosys.2025.115177","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"article","name":"content_type","label":"Content Type"},{"value":"\u00a9 2025 Elsevier B.V. All rights are reserved, including those for text and data mining, AI training, and similar technologies.","name":"copyright","label":"Copyright"}],"article-number":"115177"}}