{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,13]],"date-time":"2026-01-13T01:47:53Z","timestamp":1768268873108,"version":"3.49.0"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031712609","type":"print"},{"value":"9783031712616","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"DOI":"10.1007\/978-3-031-71261-6_7","type":"book-chapter","created":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T19:02:03Z","timestamp":1725735723000},"page":"109-126","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Extracting Formal Smart-Contract Specifications from\u00a0Natural Language with\u00a0LLMs"],"prefix":"10.1007","author":[{"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":"297","published-online":{"date-parts":[[2024,9,8]]},"reference":[{"key":"7_CR1","unstructured":"Solidity language homepage. https:\/\/soliditylang.org\/. Accessed 14 May 2024"},{"key":"7_CR2","doi-asserted-by":"publisher","unstructured":"Aceituna, D., Do, H., Srinivasan, S.: A systematic approach to transforming system requirements into model checking specifications. In: Companion Proceedings of the 36th International Conference on Software Engineering. p. 165-174. ICSE Companion 2014, Association for Computing Machinery, New York, NY, USA (2014). https:\/\/doi.org\/10.1145\/2591062.2591183, https:\/\/doi.org\/10.1145\/2591062.2591183","DOI":"10.1145\/2591062.2591183"},{"key":"7_CR3","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1007\/978-3-031-17108-6_14","volume-title":"Software Engineering and Formal Methods","author":"P Antonino","year":"2022","unstructured":"Antonino, P., Ferreira, J., Sampaio, A., Roscoe, A.W.: Specification is law: Safe creation and upgrade of ethereum smart contracts. In: Schlingloff, B.H., Chai, M. (eds.) Software Engineering and Formal Methods, pp. 227\u2013243. Springer, Cham (2022)"},{"key":"7_CR4","doi-asserted-by":"crossref","unstructured":"Antonino, P., Ferreira, J., Sampaio, A., Roscoe, A., Arruda, F.: A refinement-based approach to safe smart contract deployment and evolution. Software and Systems Modeling, pp. 1\u201337 (2024)","DOI":"10.1007\/s10270-023-01143-z"},{"key":"7_CR5","doi-asserted-by":"crossref","unstructured":"Antonino, P., Roscoe, A.: Solidifier: bounded model checking solidity using lazy contract deployment and precise memory modelling. In: Proceedings of the 36th Annual ACM Symposium on Applied Computing, pp. 1788\u20131797 (2021)","DOI":"10.1145\/3412841.3442051"},{"key":"7_CR6","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2019.102377","volume":"189","author":"F Arruda","year":"2020","unstructured":"Arruda, F., Barros, F., Sampaio, A.: Automation and consistency analysis of test cases written in natural language: an industrial context. Sci. Comput. Program. 189, 102377 (2020)","journal-title":"Sci. Comput. Program."},{"key":"7_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/978-3-319-49815-7_13","volume-title":"Formal Methods: Foundations and Applications","author":"S Barza","year":"2016","unstructured":"Barza, S., Carvalho, G., Iyoda, J., Sampaio, A., Mota, A., Barros, F.: Model checking requirements. In: Ribeiro, L., Lecomte, T. (eds.) SBMF 2016. LNCS, vol. 10090, pp. 217\u2013234. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-49815-7_13"},{"key":"7_CR8","first-page":"1877","volume":"33","author":"T Brown","year":"2020","unstructured":"Brown, T., Mann, B., Ryder, N., Subbiah, M., Kaplan, J.D., Dhariwal, P., Neelakantan, A., Shyam, P., Sastry, G., Askell, A., et al.: Language models are few-shot learners. Adv. Neural. Inf. Process. Syst. 33, 1877\u20131901 (2020)","journal-title":"Adv. Neural. Inf. Process. Syst."},{"key":"7_CR9","doi-asserted-by":"publisher","unstructured":"Carvalho, G., Cavalcanti, A., Sampaio, A.: Modelling timed reactive systems from natural-language requirements. Formal Aspects Comput. 28(5), 725\u2013765 (2016). https:\/\/doi.org\/10.1007\/S00165-016-0387-X","DOI":"10.1007\/S00165-016-0387-X"},{"key":"7_CR10","doi-asserted-by":"publisher","unstructured":"Desai, A., et al.: Program synthesis using natural language. In: Proceedings of the 38th International Conference on Software Engineering, ICSE 2016, pp. 345\u2013356. Association for Computing Machinery, New York (2016). https:\/\/doi.org\/10.1145\/2884781.2884786","DOI":"10.1145\/2884781.2884786"},{"key":"7_CR11","doi-asserted-by":"publisher","unstructured":"Feng, Z., et al.: CodeBERT: a pre-trained model for programming and natural languages. In: Cohn, T., He, Y., Liu, Y. (eds.) Findings of the Association for Computational Linguistics: EMNLP 2020, pp. 1536\u20131547. Association for Computational Linguistics, Online, November 2020. https:\/\/doi.org\/10.18653\/v1\/2020.findings-emnlp.139. https:\/\/aclanthology.org\/2020.findings-emnlp.139","DOI":"10.18653\/v1\/2020.findings-emnlp.139"},{"key":"7_CR12","doi-asserted-by":"crossref","unstructured":"Hajdu, \u00c1., Jovanovi\u0107, D.: solc-verify: A modular verifier for solidity smart contracts. In: Verified Software. Theories, Tools, and Experiments: 11th International Conference, VSTTE 2019, New York City, NY, USA, July 13\u201314, 2019, Revised Selected Papers 11, pp. 161\u2013179. Springer (2020)","DOI":"10.1007\/978-3-030-41600-3_11"},{"key":"7_CR13","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1007\/978-3-031-57259-3_13","volume-title":"Fundamental Approaches to Software Engineering","author":"C Jan\u00dfen","year":"2024","unstructured":"Jan\u00dfen, C., Richter, C., Wehrheim, H.: Can chatgpt support software verification? In: Beyer, D., Cavalcanti, A. (eds.) Fundamental Approaches to Software Engineering, pp. 266\u2013279. Springer, Cham (2024)"},{"key":"7_CR14","doi-asserted-by":"publisher","unstructured":"Leong, I.T., Barbosa, R.: Translating natural language requirements to formal specifications: a study on gpt and symbolic nlp. In: 2023 53rd Annual IEEE\/IFIP International Conference on Dependable Systems and Networks Workshops (DSN-W), pp. 259\u2013262 (2023). https:\/\/doi.org\/10.1109\/DSN-W58399.2023.00065","DOI":"10.1109\/DSN-W58399.2023.00065"},{"key":"7_CR15","doi-asserted-by":"crossref","unstructured":"Mavridou, A., Laszka, A., Stachtiari, E., Dubey, A.: Verisolid: Correct-by-design smart contracts for ethereum. In: Financial Cryptography and Data Security: 23rd International Conference, FC 2019, Frigate Bay, St. Kitts and Nevis, February 18\u201322, 2019, Revised Selected Papers 23, pp. 446\u2013465. Springer (2019)","DOI":"10.1007\/978-3-030-32101-7_27"},{"key":"7_CR16","doi-asserted-by":"publisher","unstructured":"Nogueira, S., Sampaio, A., Mota, A.: Test generation from state based use case models. Formal Asp. Comput. 26(3), 441\u2013490 (2014). https:\/\/doi.org\/10.1007\/s00165-012-0258-z","DOI":"10.1007\/s00165-012-0258-z"},{"key":"7_CR17","doi-asserted-by":"crossref","unstructured":"Permenev, A., Dimitrov, D., Tsankov, P., Drachsler-Cohen, D., Vechev, M.: Verx: safety verification of smart contracts. In: 2020 IEEE symposium on security and privacy (SP), pp. 1661\u20131677. IEEE (2020)","DOI":"10.1109\/SP40000.2020.00024"},{"key":"7_CR18","doi-asserted-by":"publisher","unstructured":"Ranta, A.: Grammatical framework. J. Funct. Program. 14(2), 145-189 (2004). https:\/\/doi.org\/10.1017\/S0956796803004738","DOI":"10.1017\/S0956796803004738"},{"key":"7_CR19","doi-asserted-by":"publisher","unstructured":"Santiago\u00a0J\u00fanior, V.A.D., Vijaykumar, N.L.: Generating model-based test cases from natural language requirements for space application software. Softw. Quality J. 20(1), 77\u2013143 (2012).https:\/\/doi.org\/10.1007\/s11219-011-9155-6","DOI":"10.1007\/s11219-011-9155-6"},{"key":"7_CR20","doi-asserted-by":"publisher","unstructured":"Selway, M., Grossmann, G., Mayer, W., Stumptner, M.: Formalising natural language specifications using a cognitive linguistic\/configuration based approach. Inf. Syst. 54, 191\u2013208 (2015). https:\/\/doi.org\/10.1016\/j.is.2015.04.003, https:\/\/www.sciencedirect.com\/science\/article\/pii\/S0306437915000630","DOI":"10.1016\/j.is.2015.04.003"},{"key":"7_CR21","unstructured":"team, C.: Claude: A next-generation ai assistant by anthropic. https:\/\/www.anthropic.com\/claude. Accessed 19 July 2024"},{"key":"7_CR22","unstructured":"Team, G., et\u00a0al.: Gemini: a family of highly capable multimodal models. arXiv preprint arXiv:2312.11805 (2023)"},{"key":"7_CR23","unstructured":"Touvron, H., et\u00a0al.: Llama 2: Open foundation and fine-tuned chat models. arXiv preprint arXiv:2307.09288 (2023)"},{"key":"7_CR24","unstructured":"Vaswani, A., Shazeer, N., Parmar, N., Uszkoreit, J., Jones, L., Gomez, A.N., Kaiser, \u0141., Polosukhin, I.: Attention is all you need. Advances in neural information processing systems 30 (2017)"},{"key":"7_CR25","doi-asserted-by":"publisher","unstructured":"Wang, C., Pastore, F., Goknil, A., Briand, L.C., Iqbal, Z.: Umtg: a toolset to automatically generate system test cases from use case specifications. In: Proceedings of the 2015 10th Joint Meeting on Foundations of Software Engineering, pp. 942\u2013945. ESEC\/FSE 2015, ACM, New York (2015). https:\/\/doi.org\/10.1145\/2786805.2803187","DOI":"10.1145\/2786805.2803187"},{"key":"7_CR26","unstructured":"Wang, Y., Lahiri, S.K., Chen, S., Pan, R., Dillig, I., Born, C., Naseer, I.: Formal specification and verification of smart contracts for azure blockchain. arXiv preprint arXiv:1812.08829 (2018)"}],"container-title":["Lecture Notes in Computer Science","Formal Aspects of Component Software"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-71261-6_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T19:02:53Z","timestamp":1725735773000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-71261-6_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031712609","9783031712616"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-71261-6_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"8 September 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FACS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Formal Aspects of Component Software","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Milan","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 September 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 September 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"facs2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/facs-conference.github.io\/2024\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}