{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T07:05:45Z","timestamp":1782889545938,"version":"3.54.5"},"publisher-location":"New York, NY, USA","reference-count":68,"publisher":"ACM","license":[{"start":{"date-parts":[[2026,6,30]],"date-time":"2026-06-30T00:00:00Z","timestamp":1782777600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc-nd\/4.0\/legalcode"}],"funder":[{"name":"State University of New York\u2019s Empire Innovation Program","award":["N\/A"],"award-info":[{"award-number":["N\/A"]}]},{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["HR00112520301"],"award-info":[{"award-number":["HR00112520301"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2026,6,30]]},"DOI":"10.1145\/3805773.3806005","type":"proceedings-article","created":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T05:20:41Z","timestamp":1782883241000},"page":"152-168","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Syntax Is Easy, Semantics Is Hard: Evaluating LLMs for LTL Translation"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1262-844X","authenticated-orcid":false,"given":"Priscilla Kyei","family":"Danso","sequence":"first","affiliation":[{"name":"Stony Brook University, Department of Computer Science, Stony Brook, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7588-8591","authenticated-orcid":false,"given":"Mohammad Saqib","family":"Hasan","sequence":"additional","affiliation":[{"name":"Stony Brook University, Department of Computer Science, Stony Brook, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4187-9368","authenticated-orcid":false,"given":"Niranjan","family":"Balasubramanian","sequence":"additional","affiliation":[{"name":"Stony Brook University, Department of Computer Science, Stony Brook, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1356-6279","authenticated-orcid":false,"given":"Omar","family":"Chowdhury","sequence":"additional","affiliation":[{"name":"Stony Brook University, Department of computer Science, Stony Brook, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,6,30]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"https:\/\/github.com\/ochowdhu\/NL2LTL- SecDev26","author":"Anonymous","unstructured":"Anonymous. 2026. Anonymous Artifact. https:\/\/github.com\/ochowdhu\/NL2LTL- SecDev26."},{"key":"e_1_3_2_1_2_1","volume-title":"SYSLITE: syntax-guided synthesis of PLTL formulas from finite traces. In # PLACEHOLDER_PARENT_METADATA_VALUE#","author":"Arif M Fareed","unstructured":"M Fareed Arif, Daniel Larraz, Mitziu Echeverria, Andrew Reynolds, Omar Chowdhury, and Cesare Tinelli. 2020. SYSLITE: syntax-guided synthesis of PLTL formulas from finite traces. In # PLACEHOLDER_PARENT_METADATA_VALUE#, Vol. 1. TU Wien Academic Press, 93-103."},{"key":"e_1_3_2_1_3_1","unstructured":"C. Baier J.P. Katoen and K.G. Larsen. 2008. Principles of Model Checking. MIT Press. https:\/\/books.google.com\/books?id=5dvxCwAAQBAJ"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.3390\/electronics14020401"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2000799.2000800"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/11901433_41"},{"key":"e_1_3_2_1_7_1","volume-title":"Leo de Penning, Gadi Pinkas, Hoifung Poon, and Gerson Zaverucha.","author":"Besold Tarek R.","year":"2017","unstructured":"Tarek R. Besold, Artur d'Avila Garcez, Sebastian Bader, Howard Bowman, Pedro Domingos, Pascal Hitzler, Kai-Uwe Kuehnberger, Luis C. Lamb, Daniel Lowd, Priscila Machado Vieira Lima, Leo de Penning, Gadi Pinkas, Hoifung Poon, and Gerson Zaverucha. 2017. Neural-Symbolic Learning and Reasoning: A Survey and Interpretation. arXiv:1711.03902 [cs.AI] https:\/\/arxiv.org\/abs\/1711.03902"},{"key":"e_1_3_2_1_8_1","unstructured":"Tom B. Brown Benjamin Mann Nick Ryder Melanie Subbiah Jared Kaplan Prafulla Dhariwal Arvind Neelakantan Pranav Shyam Girish Sastry Amanda Askell Sandhini Agarwal Ariel Herbert-Voss Gretchen Krueger Tom Henighan Rewon Child Aditya Ramesh Daniel M. Ziegler Jeffrey Wu Clemens Winter Christopher Hesse Mark Chen Eric Sigler Mateusz Litwin Scott Gray Benjamin Chess Jack Clark Christopher Berner Sam McCandlish Alec Radford Ilya Sutskever and Dario Amodei. 2020. Language Models are Few-Shot Learners. arXiv:2005.14165 [cs.CL] https:\/\/arxiv.org\/abs\/2005.14165"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/INDIN41052.2019.8972130"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/bxs102"},{"key":"e_1_3_2_1_11_1","unstructured":"Mark Chen Jerry Tworek Heewoo Jun Qiming Yuan Henrique Pinto Jared Kaplan Harri Edwards Yuri Burda Nicholas Joseph Greg Brockman et al. 2021. Evaluating large language models trained on code. arXiv preprint arXiv:2107.03374 (2021)."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2019.00043"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2462410.2462423"},{"key":"e_1_3_2_1_14_1","volume-title":"Proceedings of the 22nd ACM SIGSAC Conference on Computer and Communications Security. 1130-1143","author":"Chowdhury Omar","year":"2015","unstructured":"Omar Chowdhury, Deepak Garg, Limin Jia, and Anupam Datta. 2015. Equivalencebased Security for Querying Encrypted Databases: Theory and Application to Privacy Policy Audits. In Proceedings of the 22nd ACM SIGSAC Conference on Computer and Communications Security. 1130-1143."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.21236\/ADA609113"},{"key":"e_1_3_2_1_16_1","volume-title":"Peled","author":"Clarke Edmund M.","year":"2000","unstructured":"Edmund M. Clarke, Orna Grumberg, and Doron A. Peled. 2000. Model checking. MIT Press, Cambridge, MA, USA."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-37703-7_18"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523728"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/302405.302672"},{"key":"e_1_3_2_1_20_1","volume-title":"Syed Rafiul Hussain, and Omar Chowdhury","author":"Echeverria Mitziu","year":"2021","unstructured":"Mitziu Echeverria, Zeeshan Ahmed, Bincheng Wang, M Fareed Arif, Syed Rafiul Hussain, and Omar Chowdhury. 2021. Phoenix: Device-centric cellular network protocol monitoring using runtime verification. arXiv preprint arXiv:2101.00328 (2021)."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3734477.3734712"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-75380-0_7"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.3233\/978-1-61499-627-9-72"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1002\/9781119991472"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1291535.1291542"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v37i13.27068"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.TIME.2021.8"},{"key":"e_1_3_2_1_28_1","volume-title":"Hu","author":"Gouglidis Antonios","year":"2023","unstructured":"Antonios Gouglidis, Anna Kagia, and Vincent C. Hu. 2023. Model Checking Access Control Policies: A Case Study using Google Cloud IAM. arXiv:2303.16688 [cs.CR] https:\/\/arxiv.org\/abs\/2303.16688"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.22152\/programmingjournal.org\/2023\/7\/7"},{"key":"e_1_3_2_1_30_1","volume-title":"CloudFix: Automated Policy Repair for Cloud Access Control Policies Using Large Language Models. arXiv:2512.09957","author":"Hall Bethel","year":"2025","unstructured":"Bethel Hall, Owen Ungaro, and William Eiers. 2025. CloudFix: Automated Policy Repair for Cloud Access Control Policies Using Large Language Models. arXiv:2512.09957 (2025)."},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/DSN.2017.36"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.14722\/ndss.2018.23313"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3319535.3354263"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3460120.3485388"},{"key":"e_1_3_2_1_35_1","volume-title":"Formal Logic: Its Scope and Limits","author":"Jeffrey R.C.","year":"2006","unstructured":"R.C. Jeffrey and J.P. Burgess. 2006. Formal Logic: Its Scope and Limits. Hackett Publishing Company. https:\/\/books.google.com\/books?id=iqvsjhvZCgcC"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1111\/nyas.15125"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-23820-3_7"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2005.1553580"},{"key":"e_1_3_2_1_40_1","first-page":"209","article-title":"CRV: Automated Cyber-Resiliency Reasoning for System Design Models. In 2023 Formal Methods in Computer-Aided Design (FMCAD)","author":"Larraz Daniel","year":"2023","unstructured":"Daniel Larraz, Robert Lorch, Moosa Yahyazadeh, M Fareed Arif, Omar Chowdhury, and Cesare Tinelli. 2023. CRV: Automated Cyber-Resiliency Reasoning for System Design Models. In 2023 Formal Methods in Computer-Aided Design (FMCAD). IEEE, 209-220.","journal-title":"IEEE"},{"key":"e_1_3_2_1_41_1","volume-title":"Ahsan Benhalloum, Miltiadis Allamanis, Aqsa Bibi, Federico Cassano, Charles Chausson, Debajyoti Dey, Iddo Drori, and et al.","author":"Li Raymond","year":"2023","unstructured":"Raymond Li, Loubna Ben Allal, Ahsan Benhalloum, Miltiadis Allamanis, Aqsa Bibi, Federico Cassano, Charles Chausson, Debajyoti Dey, Iddo Drori, and et al. 2023. StarCoder: may the source be with you! Transactions on Machine Learning Research (2023). https:\/\/openreview.net\/forum?id=GZwT6KAF0Y OpenReview preprint."},{"key":"e_1_3_2_1_42_1","first-page":"196","volume-title":"Proceedings of the Conference on Logic of Programs. Springer-Verlag","author":"Lichtenstein Orna","unstructured":"Orna Lichtenstein, Amir Pnueli, and Lenore D. Zuck. 1985. The Glory of the Past. In Proceedings of the Conference on Logic of Programs. Springer-Verlag, Berlin, Heidelberg, 196-218."},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3678890.3678927"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3551349.3561163"},{"key":"e_1_3_2_1_45_1","first-page":"46534","volume-title":"Levine (Eds.)","volume":"36","author":"Madaan Aman","year":"2023","unstructured":"Aman Madaan, Niket Tandon, Prakhar Gupta, Skyler Hallinan, Luyu Gao, Sarah Wiegreffe, Uri Alon, Nouha Dziri, Shrimai Prabhumoye, Yiming Yang, Shashank Gupta, Bodhisattwa Prasad Majumder, Katherine Hermann, Sean Welleck, Amir Yazdanbakhsh, and Peter Clark. 2023. Self-Refine: Iterative Refinement with Self-Feedback. In Advances in Neural Information Processing Systems, A. Oh, T. Naumann, A. Globerson, K. Saenko, M. Hardt, and S. Levine (Eds.), Vol. 36. Curran Associates, Inc., 46534-46594. https:\/\/proceedings.neurips.cc\/paper_fil es\/paper\/2023\/file\/91edff07232fb1b55a505a9e9f6c0ff3-Paper-Conference.pdf"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30206-3_12"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3558482.3590188"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3510003.3510082"},{"key":"e_1_3_2_1_49_1","unstructured":"William Murphy Nikolaus Holzer Nathan Koenig Leyi Cui Raven Rothkopf Feitong Qiao and Mark Santolucito. 2024. Guiding LLM Temporal Logic Generation with Explicit Separation of Data and Control. arXiv:2406.07400 [cs.LG] https:\/\/arxiv.org\/abs\/2406.07400"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1109\/IECON51785.2023.10311970"},{"key":"e_1_3_2_1_51_1","volume-title":"Flexible and Efficient Grammar-Constrained Decoding. In Forty-second International Conference on Machine Learning. https:\/\/openreview.net\/forum?id=L6CYAzpO1k","author":"Park Kanghee","year":"2025","unstructured":"Kanghee Park, Timothy Zhou, and Loris D'Antoni. 2025. Flexible and Efficient Grammar-Constrained Decoding. In Forty-second International Conference on Machine Learning. https:\/\/openreview.net\/forum?id=L6CYAzpO1k"},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-71167-1_2"},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_3_2_1_54_1","volume-title":"The Fourteenth International Conference on Learning Representations. https:\/\/openreview.net\/forum?id=NChBLvOr7I","author":"Quansah Paapa Kwesi","year":"2026","unstructured":"Paapa Kwesi Quansah, Pablo Rivas, and Ernest Bonnah. 2026. VERIFY: A Novel Multi-Domain Dataset Grounding LTL in Contextual Natural Language via Provable Intermediate Logic. In The Fourteenth International Conference on Learning Representations. https:\/\/openreview.net\/forum?id=NChBLvOr7I"},{"key":"e_1_3_2_1_55_1","volume-title":"Md Tanjum An Tashrif, Airin Afroj Aishi, Md Ahsan Karim, Dipanjali Kundu, Tanoy Debnath, Md. Abul Ala Moududi, and MD. Zunead Abedin Eidmum.","author":"Rahman Anichur","year":"2025","unstructured":"Anichur Rahman, Shahariar Hossain Mahir, Md Tanjum An Tashrif, Airin Afroj Aishi, Md Ahsan Karim, Dipanjali Kundu, Tanoy Debnath, Md. Abul Ala Moududi, and MD. Zunead Abedin Eidmum. 2025. Comparative Analysis Based on DeepSeek, ChatGPT, and Google Gemini: Features, Techniques, Performance, Future Prospects. arXiv:2503.04783 [cs.CL] https:\/\/arxiv.org\/abs\/2503.04783"},{"key":"e_1_3_2_1_56_1","volume-title":"Proceedings of the 2024 on ACM SIGSAC Conference on Computer and Communications Security. 2102-2116","author":"Mukit Rashid Syed Md","year":"2024","unstructured":"Syed Md Mukit Rashid, Tianwei Wu, Kai Tu, Abdullah Al Ishtiaq, Ridwanul Hasan Tanvir, Yilu Dong, Omar Chowdhury, and Syed Rafiul Hussain. 2024. State machine mutation-based testing framework for wireless communication protocols. In Proceedings of the 2024 on ACM SIGSAC Conference on Computer and Communications Security. 2102-2116."},{"key":"e_1_3_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.iotcps.2023"},{"key":"e_1_3_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/3643737"},{"key":"e_1_3_2_1_59_1","unstructured":"Weizhi Tang and Vaishak Belle. 2024. LTLBench: Towards Benchmarks for Evaluating Temporal Logic Reasoning in Large Language Models. arXiv:2407.05434 [cs.CL] https:\/\/arxiv.org\/abs\/2407.05434"},{"key":"e_1_3_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.18653\/v1\/2021.emnlp-main.685"},{"key":"e_1_3_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.5555\/3600270.3602070"},{"key":"e_1_3_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1109\/QRS62785.2024.00029"},{"key":"e_1_3_2_1_63_1","volume-title":"Endadul Hoque, and Omar Chowdhury.","author":"Yahyazadeh Moosa","year":"2020","unstructured":"Moosa Yahyazadeh, Syed Rafiul Hussain, Endadul Hoque, and Omar Chowdhury. 2020. PatrIoT: Policy Assisted Resilient Programmable IoT System. In Runtime Verification, Jyotirmoy Deshmukh and Dejan Ni\u010dkovi\u0107 (Eds.). Springer International Publishing, Cham, 151-171."},{"key":"e_1_3_2_1_64_1","doi-asserted-by":"crossref","unstructured":"Yao Yao Zuchao Li and Hai Zhao. 2024. Beyond Chain-of-Thought Effective Graph-of-Thought Reasoning in Language Models. arXiv:2305.16582 [cs.CL] https:\/\/arxiv.org\/abs\/2305.16582","DOI":"10.18653\/v1\/2024.findings-naacl.183"},{"key":"e_1_3_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACSACW65225.2024.00033"},{"key":"e_1_3_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACSACW65225.2024.00033"},{"key":"e_1_3_2_1_67_1","unstructured":"Yedi Zhang Yufan Cai Xinyue Zuo Xiaokun Luan Kailong Wang Zhe Hou Yifan Zhang Zhiyuan Wei Meng Sun Jun Sun Jing Sun and Jin Song Dong. 2024. The Fusion of Large Language Models and Formal Methods for Trustworthy AI Agents: A Roadmap. arXiv:2412.06512 [cs.AI] https:\/\/arxiv.org\/abs\/2412.06512"},{"key":"e_1_3_2_1_68_1","volume-title":"Chi","author":"Zhou Denny","year":"2023","unstructured":"Denny Zhou, Nathanael Sch\u00e4rli, Le Hou, Jason Wei, Nathan Scales, Xuezhi Wang, Dale Schuurmans, Claire Cui, Olivier Bousquet, Quoc Le, and Ed Chi. 2023. Least-to-Most Prompting Enables Complex Reasoning in Large Language Models. arXiv:2205.10625 [cs.AI] https:\/\/arxiv.org\/abs\/2205.10625"}],"event":{"name":"SecDev '26: 2026 ACM Secure Development Conference","location":"Montreal QC Canada","acronym":"SecDev '26","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering"]},"container-title":["Proceedings of the 2026 ACM Secure Development Conference"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3805773.3806005","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3805773.3806005","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T05:29:54Z","timestamp":1782883794000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3805773.3806005"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,6,30]]},"references-count":68,"alternative-id":["10.1145\/3805773.3806005","10.1145\/3805773"],"URL":"https:\/\/doi.org\/10.1145\/3805773.3806005","relation":{},"subject":[],"published":{"date-parts":[[2026,6,30]]},"assertion":[{"value":"2026-06-30","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}