{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,7]],"date-time":"2026-02-07T13:50:26Z","timestamp":1770472226052,"version":"3.49.0"},"reference-count":26,"publisher":"IEEE","license":[{"start":{"date-parts":[[2024,10,3]],"date-time":"2024-10-03T00:00:00Z","timestamp":1727913600000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2024,10,3]],"date-time":"2024-10-03T00:00:00Z","timestamp":1727913600000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"funder":[{"DOI":"10.13039\/501100004489","name":"Mitacs","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100004489","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024,10,3]]},"DOI":"10.1109\/rsp64122.2024.10870993","type":"proceedings-article","created":{"date-parts":[[2025,2,11]],"date-time":"2025-02-11T18:20:48Z","timestamp":1739298048000},"page":"21-27","source":"Crossref","is-referenced-by-count":3,"title":["Advancing Formal Verification: Fine-Tuning LLMs for Translating Natural Language Requirements to CTL Specifications"],"prefix":"10.1109","author":[{"given":"Rim","family":"Zrelli","sequence":"first","affiliation":[{"name":"Polytechnique Montreal,Computer Engineering and Software Engineering Department,Montreal,Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Henrique Amaral","family":"Misson","sequence":"additional","affiliation":[{"name":"Polytechnique Montreal,Computer Engineering and Software Engineering Department,Montreal,Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Maroua","family":"Ben Attia","sequence":"additional","affiliation":[{"name":"Research &amp; Development Humanitas Solutions,Montreal,Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Felipe Gohring","family":"de Magalhaes","sequence":"additional","affiliation":[{"name":"Polytechnique Montreal,Computer Engineering and Software Engineering Department,Montreal,Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Abdo","family":"Shabah","sequence":"additional","affiliation":[{"name":"Research &amp; Development Humanitas Solutions,Montreal,Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gabriela","family":"Nicolescu","sequence":"additional","affiliation":[{"name":"Polytechnique Montreal,Computer Engineering and Software Engineering Department,Montreal,Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1109\/INDIN41052.2019.8972130"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-57327-9_13"},{"key":"ref3","volume-title":"Principles of model checking","author":"Baier","year":"2008"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1007\/978-81-322-3972-7_19"},{"key":"ref5","first-page":"1877","article-title":"Language models are few-shot learners","volume":"33","author":"Brown","year":"2020","journal-title":"Advances in neural information processing systems"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1007\/s11704-016-6192-0"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48958-4_1"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1145\/3695988"},{"key":"ref9","first-page":"40","article-title":"From natural language requirements to rigorous property specifications","volume-title":"Workshop on Software Engineering for Embedded Systems (SEES 2003): From Requirements to Implementation","author":"Smith"},{"key":"ref10","article-title":"Extracting formal specifications from natural language regulatory documents","volume-title":"Proceedings of the Fifth International Workshop on Inference in Computational Semantics (ICoS-5)","author":"Dinesh"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1109\/ICTAI.2013.116"},{"key":"ref12","article-title":"Automatically extracting requirements specifications from natural language","author":"Ghosh","year":"2014"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1109\/ICOSC.2015.7050777"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1145\/302405.302672"},{"key":"ref15","first-page":"99","article-title":"Structured english for model checking specification","volume-title":"MBMV","author":"Flake","year":"2000"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2005.1553580"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1163\/156855308X344864"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1109\/ROBOT.2009.5152776"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.18653\/v1\/2021.blackboxnlp-1.31"},{"key":"ref20","article-title":"Formal specifications from natural language","author":"Hahn","year":"2022"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1109\/ATS56056.2022.00034"},{"key":"ref22","article-title":"Lang2ltl: Translating natural language commands to temporal specification with large language models","volume-title":"Workshop on Language and Robotics at CoRL 2022","author":"Liu"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-37703-7_18"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.18653\/v1\/2023.emnlp-main.985"},{"key":"ref25","first-page":"32353","article-title":"Autoformalization with large language models","volume":"35","author":"Wu","year":"2022","journal-title":"Advances in Neural Information Processing Systems"},{"key":"ref26","first-page":"arXiv\u20132309","article-title":"Using llms to facilitate formal verification of rtl","author":"Orenes-Vera","year":"2023"}],"event":{"name":"2024 IEEE International Workshop on Rapid System Prototyping (RSP)","location":"Raleigh, NC, USA","start":{"date-parts":[[2024,10,3]]},"end":{"date-parts":[[2024,10,3]]}},"container-title":["2024 International Workshop on Rapid System Prototyping (RSP)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx8\/10870368\/10870893\/10870993.pdf?arnumber=10870993","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,12]],"date-time":"2025-02-12T07:09:36Z","timestamp":1739344176000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/10870993\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,3]]},"references-count":26,"URL":"https:\/\/doi.org\/10.1109\/rsp64122.2024.10870993","relation":{},"subject":[],"published":{"date-parts":[[2024,10,3]]}}}