{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,25]],"date-time":"2026-04-25T13:55:17Z","timestamp":1777125317827,"version":"3.51.4"},"reference-count":52,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T00:00:00Z","timestamp":1782864000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T00:00:00Z","timestamp":1782864000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"},{"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-017"},{"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"},{"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-012"},{"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-004"}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Science of Computer Programming"],"published-print":{"date-parts":[[2026,7]]},"DOI":"10.1016\/j.scico.2026.103464","type":"journal-article","created":{"date-parts":[[2026,2,23]],"date-time":"2026-02-23T16:52:10Z","timestamp":1771865530000},"page":"103464","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":0,"special_numbering":"C","title":["Generating formal smart-contract specifications: comparing few-shot learning and fine-tuned LLMs"],"prefix":"10.1016","volume":"252","author":[{"ORCID":"https:\/\/orcid.org\/0009-0007-0232-8076","authenticated-orcid":false,"given":"Gabriel","family":"Leite","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-1111-9142","authenticated-orcid":false,"given":"Filipe","family":"Arruda","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5627-0910","authenticated-orcid":false,"given":"Pedro","family":"Antonino","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6593-577X","authenticated-orcid":false,"given":"Augusto","family":"Sampaio","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7557-3901","authenticated-orcid":false,"given":"A.W.","family":"Roscoe","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/j.scico.2026.103464_bib0001","unstructured":"Y. Wang, S. K. Lahiri, S. Chen, R. Pan, I. Dillig, C. Born, I. Naseer, Formal specification and verification of smart contracts for azure blockchain, arXiv: 1812.08829(2018)."},{"key":"10.1016\/j.scico.2026.103464_bib0002","series-title":"Financial Cryptography and Data Security: 23rd International Conference, FC 2019, Frigate Bay, St. Kitts and Nevis, February 18\u201322, 2019, Revised Selected Papers 23","first-page":"446","article-title":"VeriSolid: correct-by-design smart contracts for ethereum","author":"Mavridou","year":"2019"},{"key":"10.1016\/j.scico.2026.103464_bib0003","series-title":"Verified Software. Theories, Tools, and Experiments: 11th International Conference, VSTTE 2019, New York City, NY, USA, July 13\u201314, 2019, Revised Selected Papers 11","first-page":"161","article-title":"solc-verify: a modular verifier for solidity smart contracts","author":"Hajdu","year":"2020"},{"key":"10.1016\/j.scico.2026.103464_bib0004","series-title":"2020 IEEE Symposium on Security and Privacy (SP)","first-page":"1661","article-title":"Verx: safety verification of smart contracts","author":"Permenev","year":"2020"},{"key":"10.1016\/j.scico.2026.103464_bib0005","series-title":"Proceedings of the 36th Annual ACM Symposium on Applied Computing","first-page":"1788","article-title":"Solidifier: bounded model checking solidity using lazy contract deployment and precise memory modelling","author":"Antonino","year":"2021"},{"key":"10.1016\/j.scico.2026.103464_bib0006","series-title":"Findings of the Association for Computational Linguistics: EMNLP 2020","first-page":"1536","article-title":"CodeBERT: a pre-Trained model for programming and natural languages","author":"Feng","year":"2020"},{"key":"10.1016\/j.scico.2026.103464_bib0007","series-title":"Proceedings of the 38th International Conference on Software Engineering","first-page":"345","article-title":"Program synthesis using natural language","author":"Desai","year":"2016"},{"key":"10.1016\/j.scico.2026.103464_bib0008","series-title":"Formal Methods: Foundations and Applications - 19th Brazilian Symposium, SBMF 2016, Natal, Brazil, November 23\u201325, 2016, Proceedings","first-page":"217","article-title":"Model checking requirements","volume":"10090","author":"Barza","year":"2016"},{"issue":"5","key":"10.1016\/j.scico.2026.103464_bib0009","doi-asserted-by":"crossref","first-page":"725","DOI":"10.1007\/s00165-016-0387-x","article-title":"Modelling timed reactive systems from natural-language requirements","volume":"28","author":"Carvalho","year":"2016","journal-title":"Formal Aspects Comput."},{"key":"10.1016\/j.scico.2026.103464_bib0010","series-title":"Proceedings of the 2015 10th Joint Meeting on Foundations of Software Engineering","first-page":"942","article-title":"UMTG: a toolset to automatically generate system test cases from use case specifications","author":"Wang","year":"2015"},{"issue":"3","key":"10.1016\/j.scico.2026.103464_bib0011","doi-asserted-by":"crossref","first-page":"441","DOI":"10.1007\/s00165-012-0258-z","article-title":"Test generation from state based use case models","volume":"26","author":"Nogueira","year":"2014","journal-title":"Formal Asp. Comput."},{"key":"10.1016\/j.scico.2026.103464_bib0012","doi-asserted-by":"crossref","DOI":"10.1016\/j.scico.2019.102377","article-title":"Automation and consistency analysis of test cases written in natural language: an industrial context","volume":"189","author":"Arruda","year":"2020","journal-title":"Sci. Comput. Program."},{"key":"10.1016\/j.scico.2026.103464_bib0013","first-page":"5998","article-title":"Attention is all you need","volume":"30","author":"Vaswani","year":"2017","journal-title":"Adv. Neural Inf. Process. Syst."},{"key":"10.1016\/j.scico.2026.103464_bib0014","first-page":"1877","article-title":"Language models are few-shot learners","volume":"33","author":"Brown","year":"2020","journal-title":"Adv. Neural Inf. Process. Syst."},{"key":"10.1016\/j.scico.2026.103464_bib0015","series-title":"Proceedings of the 39th IEEE\/ACM International Conference on Automated Software Engineering","first-page":"2294","article-title":"Translation titans, reasoning challenges: satisfiability-aided language models for detecting conflicting requirements","author":"Fazelnia","year":"2024"},{"issue":"3","key":"10.1016\/j.scico.2026.103464_bib0016","doi-asserted-by":"crossref","first-page":"781","DOI":"10.1007\/s10270-023-01105-5","article-title":"On the assessment of generative AI in modeling tasks: an experience report with chatGPT and UML","volume":"22","author":"C\u00e1mara","year":"2023","journal-title":"Softw. Syst. Model."},{"key":"10.1016\/j.scico.2026.103464_sbref0017","doi-asserted-by":"crossref","first-page":"1330","DOI":"10.1162\/tacl_a_00694","article-title":"Novicode: generating programs from natural language utterances by novices","volume":"12","author":"Mordechai","year":"2024","journal-title":"Trans. Assoc. Comput. Linguist."},{"key":"10.1016\/j.scico.2026.103464_bib0018","series-title":"2025 IEEE\/ACM 47th International Conference on Software Engineering (ICSE)","first-page":"779","article-title":"Test intention guided LLM-based unit test generation","author":"Nan","year":"2025"},{"key":"10.1016\/j.scico.2026.103464_bib0019","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.scico.2026.103464_bib0020","series-title":"2025 IEEE\/ACM 47th International Conference on Software Engineering (ICSE)","first-page":"734","article-title":"LLM-aided automatic modelling for security protocol verification","author":"Mao","year":"2025"},{"key":"10.1016\/j.scico.2026.103464_bib0021","series-title":"Fundamental Approaches to Software Engineering","first-page":"266","article-title":"Can chatGPT support software verification?","author":"Jan\u00dfen","year":"2024"},{"key":"10.1016\/j.scico.2026.103464_bib0022","series-title":"Proceedings of the 39th IEEE\/ACM International Conference on Automated Software Engineering","first-page":"406","article-title":"LLM meets bounded model checking: neuro-symbolic loop invariant inference","author":"Wu","year":"2024"},{"key":"10.1016\/j.scico.2026.103464_bib0023","unstructured":"S. Team, Solidity language homepage, 2024, https:\/\/soliditylang.org\/. Accessed: 2024-05-14."},{"key":"10.1016\/j.scico.2026.103464_bib0024","series-title":"Software Engineering and Formal Methods","first-page":"227","article-title":"Specification is law: safe creation and upgrade of ethereum smart contracts","author":"Antonino","year":"2022"},{"key":"10.1016\/j.scico.2026.103464_bib0025","doi-asserted-by":"crossref","first-page":"657","DOI":"10.1007\/s10270-023-01143-z","article-title":"A refinement-based approach to safe smart contract deployment and evolution","volume":"23","author":"Antonino","year":"2024","journal-title":"Softw. Syst. Model."},{"key":"10.1016\/j.scico.2026.103464_bib0026","series-title":"Formal Aspects of Component Software - 20th International Conference, FACS 2024, Milan, Italy, September 9\u201310, 2024, Proceedings","first-page":"109","article-title":"Extracting formal smart-Contract specifications from natural language with LLMs","volume":"15189","author":"Leite","year":"2024"},{"key":"10.1016\/j.scico.2026.103464_bib0027","unstructured":"M. Shoeybi, M. Patwary, R. Puri, P. LeGresley, J. Casper, B. Catanzaro, Megatron-lm: training multi-billion parameter language models using model parallelism, (2019). arXiv: 1909.08053."},{"key":"10.1016\/j.scico.2026.103464_bib0028","unstructured":"M. Chen, J. Tworek, H. Jun, Q. Yuan, P.H.P.D. Oliveira, J. Kaplan, H. Edwards, Y. Burda, N. Joseph, G. Brockman, et al., Evaluating large language models trained on code, (2021). arXiv: 2107.03374."},{"key":"10.1016\/j.scico.2026.103464_bib0029","unstructured":"P. Sahoo, A.K. Singh, S. Saha, V. Jain, S. Mondal, A. Chadha, A systematic survey of prompt engineering in large language models: techniques and applications, (2024). arXiv: 2402.07927."},{"key":"10.1016\/j.scico.2026.103464_bib0030","series-title":"Improving Language Understanding by Generative Pre-Training","author":"Radford","year":"2018"},{"key":"10.1016\/j.scico.2026.103464_sbref0031","series-title":"Proceedings of the 59th Annual Meeting of the Association for Computational Linguistics (ACL)","first-page":"1568","article-title":"On the stability of fine-tuning BERT: misconceptions, explanations, and strong baselines","author":"Mosbach","year":"2021"},{"key":"10.1016\/j.scico.2026.103464_bib0032","article-title":"An in-depth study to fine-tune the hyperparameters of pre-trained transformers","year":"2024","journal-title":"Neural Comput. Appl."},{"key":"10.1016\/j.scico.2026.103464_bib0033","unstructured":"M. Marek, S. Lotfi, A. Somasundaram, M. Goldblum, A.G. Wilson, Small batch size training for language models: when vanilla SGD works, and why gradient accumulation is wasteful, (2025). arXiv: 2507.07101https:\/\/arxiv.org\/html\/2507.07101v2."},{"issue":"1994","key":"10.1016\/j.scico.2026.103464_bib0034","first-page":"528","article-title":"The goal question metric approach","volume":"2","author":"Caldiera","year":"1994","journal-title":"Encycloped. Softw. Eng."},{"key":"10.1016\/j.scico.2026.103464_bib0035","unstructured":"Y. Sun, Y. Zhang, Z. Zhao, S. Wan, D. Tao, C. Gong, Fast-Slow-Thinking: Complex Task Solving with Large Language Models, (2025). arXiv: 2504.08690."},{"issue":"2","key":"10.1016\/j.scico.2026.103464_bib0036","doi-asserted-by":"crossref","first-page":"145","DOI":"10.1017\/S0956796803004738","article-title":"Grammatical framework","volume":"14","author":"Ranta","year":"2004","journal-title":"J. Funct. Program."},{"key":"10.1016\/j.scico.2026.103464_bib0037","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1016\/j.is.2015.04.003","article-title":"Formalising natural language specifications using a cognitive linguistic\/configuration based approach","volume":"54","author":"Selway","year":"2015","journal-title":"Inf. Syst."},{"key":"10.1016\/j.scico.2026.103464_bib0038","series-title":"Companion Proceedings of the 36th International Conference on Software Engineering","first-page":"165","article-title":"A systematic approach to transforming system requirements into model checking specifications","author":"Aceituna","year":"2014"},{"issue":"1","key":"10.1016\/j.scico.2026.103464_bib0039","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1007\/s11219-011-9155-6","article-title":"Generating model-based test cases from natural language requirements for space application software","volume":"20","author":"Santiago J\u00fanior","year":"2012","journal-title":"Softw. Qual. J."},{"key":"10.1016\/j.scico.2026.103464_bib0040","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.scico.2026.103464_bib0041","doi-asserted-by":"crossref","unstructured":"N.F. Liu, K. Lin, J. Hewitt, A. Paranjape, M. Bevilacqua, F. Petroni, P. Liang, Lost in the middle: how language models use long contexts, (2023). arXiv: 2307.03172.","DOI":"10.1162\/tacl_a_00638"},{"key":"10.1016\/j.scico.2026.103464_bib0042","series-title":"Proceedings of the 39th IEEE\/ACM International Conference on Automated Software Engineering","first-page":"406","article-title":"LLM meets bounded model checking: neuro-symbolic loop invariant inference","author":"Wu","year":"2024"},{"key":"10.1016\/j.scico.2026.103464_bib0043","unstructured":"L. Ma, S. Liu, Y. Li, X. Xie, L. Bu, Specgen: automated generation of formal program specifications via large language models, (2024). arXiv: 2401.08807."},{"key":"10.1016\/j.scico.2026.103464_bib0044","doi-asserted-by":"crossref","unstructured":"J. Cao, Y. Lu, M. Li, H. Ma, H. Li, M. He, C. Wen, L. Sun, H. Zhang, S. Qin, et al., From informal to formal\u2013incorporating and evaluating LLMs on natural language requirements to verifiable formal proofs, (2025). arXiv: 2501.16207.","DOI":"10.32388\/MLAOTG"},{"key":"10.1016\/j.scico.2026.103464_bib0045","unstructured":"Certora Inc., Certora verification language (CVL) documentation, 2025, https:\/\/docs.certora.com. Accessed: 2025-09-05."},{"key":"10.1016\/j.scico.2026.103464_bib0046","doi-asserted-by":"crossref","unstructured":"Y. Liu, Y. Xue, D. Wu, Y. Sun, Y. Li, M. Shi, Y. Liu, Propertygpt: llm-driven formal verification of smart contracts through retrieval-augmented property generation, (2024). arXiv: 2405.02580.","DOI":"10.14722\/ndss.2025.241357"},{"key":"10.1016\/j.scico.2026.103464_bib0047","unstructured":"S. Xia, M. He, S. Shao, T. Yu, Y. Zhang, L. Song, SymGPT: auditing smart contracts via combining symbolic execution with large language models, (2025). arXiv: 2502.07644."},{"key":"10.1016\/j.scico.2026.103464_bib0048","unstructured":"G. Team, R. Anil, S. Borgeaud, Y. Wu, J.-B. Alayrac, J. Yu, R. Soricut, J. Schalkwyk, A.M. Dai, A. Hauth, et al., Gemini: a family of highly capable multimodal models, (2023). arXiv: 2312.11805."},{"key":"10.1016\/j.scico.2026.103464_bib0049","unstructured":"H. Touvron, L. Martin, K. Stone, P. Albert, A. Almahairi, Y. Babaei, N. Bashlykov, S. Batra, P. Bhargava, S. Bhosale, et al., Llama 2: open foundation and fine-tuned chat models, (2023). arXiv: 2307.09288."},{"key":"10.1016\/j.scico.2026.103464_bib0050","unstructured":"C. team, Claude: a next-generation AI assistant by anthropic, 2024. Accessed: 2024-07-19, https:\/\/www.anthropic.com\/claude."},{"key":"10.1016\/j.scico.2026.103464_bib0051","unstructured":"M. Bartoletti, E. Lipparini, L. Pompianu, LLMs as verification oracles for Solidity, (2025). arXiv: 2509.19153."},{"key":"10.1016\/j.scico.2026.103464_bib0052","unstructured":"Z. Ye, Z. Yan, J. He, T. Kasriel, K. Yang, D. Song, VERINA: benchmarking verifiable code generation, (2025). arXiv: 2505.23135."}],"container-title":["Science of Computer Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0167642326000304?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0167642326000304?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2026,4,25]],"date-time":"2026-04-25T13:30:47Z","timestamp":1777123847000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0167642326000304"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,7]]},"references-count":52,"alternative-id":["S0167642326000304"],"URL":"https:\/\/doi.org\/10.1016\/j.scico.2026.103464","relation":{},"ISSN":["0167-6423"],"issn-type":[{"value":"0167-6423","type":"print"}],"subject":[],"published":{"date-parts":[[2026,7]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Generating formal smart-contract specifications: comparing few-shot learning and fine-tuned LLMs","name":"articletitle","label":"Article Title"},{"value":"Science of Computer Programming","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/j.scico.2026.103464","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"article","name":"content_type","label":"Content Type"},{"value":"\u00a9 2026 Published by Elsevier B.V.","name":"copyright","label":"Copyright"}],"article-number":"103464"}}