{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,18]],"date-time":"2026-07-18T02:37:54Z","timestamp":1784342274544,"version":"3.55.0"},"publisher-location":"New York, NY, USA","reference-count":42,"publisher":"ACM","license":[{"start":{"date-parts":[[2023,12,8]],"date-time":"2023-12-08T00:00:00Z","timestamp":1701993600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2023,12,8]]},"DOI":"10.1145\/3617555.3617874","type":"proceedings-article","created":{"date-parts":[[2023,12,1]],"date-time":"2023-12-01T03:27:53Z","timestamp":1701401273000},"page":"33-43","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":60,"title":["The FormAI Dataset: Generative AI in Software Security through the Lens of Formal Verification"],"prefix":"10.1145","author":[{"given":"Norbert","family":"Tihanyi","sequence":"first","affiliation":[{"name":"Technology Innovation Institute, Abu Dhabi, United Arab Emirates"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Tamas","family":"Bisztray","sequence":"additional","affiliation":[{"name":"University of Oslo, Oslo, Norway"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ridhi","family":"Jain","sequence":"additional","affiliation":[{"name":"Technology Innovation Institute, Abu Dhabi, United Arab Emirates"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mohamed Amine","family":"Ferrag","sequence":"additional","affiliation":[{"name":"Technology Innovation Institute, Abu Dhabi, United Arab Emirates"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Lucas C.","family":"Cordeiro","sequence":"additional","affiliation":[{"name":"University of Manchester, Manchester, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Vasileios","family":"Mavroeidis","sequence":"additional","affiliation":[{"name":"University of Oslo, Oslo, Norway"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2023,12,8]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Ullman","author":"Aho Alfred V.","year":"2006","unstructured":"Alfred V. Aho, Monica S. Lam, Ravi Sethi, and Jeffrey D. Ullman. 2006. Compilers: Principles, Techniques, And Tools (2nd ed.). Addison-Wesley Longman Publishing Co., Inc., Boston, MA."},{"key":"e_1_3_2_1_2_1","volume-title":"Competition on Software Verification and Witness Validation: SV-COMP","author":"Beyer Dirk","year":"2023","unstructured":"Dirk Beyer. 2023. Competition on Software Verification and Witness Validation: SV-COMP 2023. In Tools and Algorithms for the Construction and Analysis of Systems, Sriram Sankaranarayanan and Natasha Sharygina (Eds.). Springer Nature Switzerland, Cham. 495\u2013522. isbn:978-3-031-30820-8"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.6028\/jres.123.005"},{"key":"e_1_3_2_1_4_1","volume-title":"Akhilesh Deepak Gotmare, and Steven C. H. Hoi","author":"Bui Nghi D. Q.","year":"2023","unstructured":"Nghi D. Q. Bui, Hung Le, Yue Wang, Junnan Li, Akhilesh Deepak Gotmare, and Steven C. H. Hoi. 2023. CodeTF: One-stop Transformer Library for State-of-the-art Code LLM. arxiv:2306.00029"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2021.3087402"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2305.14752"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ajog.2023.03.010"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"crossref","unstructured":"Yizheng Chen Zhoujie Ding Xinyun Chen and David Wagner. 2023. DiverseVul: A New Vulnerable Source Code Dataset for Deep Learning Based Vulnerability Detection. arxiv:2304.00409","DOI":"10.1145\/3607199.3607242"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2011.59"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/48529.48530"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2008.923410"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3379597.3387501"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3238147.3240481"},{"key":"e_1_3_2_1_14_1","volume-title":"Nicole","author":"Gadelha Mikhail R.","year":"2023","unstructured":"Mikhail R. Gadelha, Felipe R. Monteiro, Jeremy Morse, Lucas C. Cordeiro, Bernd Fischer, and Denis A. Nicole. 2023. ESBMC: 5.0: An Industrial-Strength Model Checker. https:\/\/github.com\/esbmc\/esbmc original-date: 2015-06-20T19:35:34Z"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE-Companion.2019.00026"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2303.05398"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3578527.3578530"},{"key":"e_1_3_2_1_18_1","volume-title":"Boland Jr and Paul E. Black","author":"Frederick","year":"2012","unstructured":"Frederick E. Boland Jr and Paul E. Black. 2012. The Juliet 1.1 C\/C++ and Java Test Suite. NIST, 45, 10 (2012), Oct., 88\u201390. https:\/\/www.nist.gov\/publications\/juliet-11-cc-and-java-test-suite Last Modified: 2021-10-12T11:10-04:00 Publisher: Frederick E. Boland Jr., Paul E. Black"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"crossref","unstructured":"Rapha\u00ebl Khoury Anderson R. Avila Jacob Brunelle and Baba Mamadou Camara. 2023. How Secure is Code Generated by ChatGPT? arxiv:2304.09655","DOI":"10.1109\/SMC53992.2023.10394237"},{"key":"e_1_3_2_1_20_1","unstructured":"Louis Kim and Rebecca Russell. 2018. Draper VDISC Dataset - Vulnerability Detection in Source Code. https:\/\/osf.io\/d45bw\/ Publisher: OSF"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_26"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2305.01210"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","unstructured":"Wei Ma Shangqing Liu Wenhan Wang Qiang Hu Ye Liu Cen Zhang Liming Nie and Yang Liu. 2023. The Scope of ChatGPT in Software Engineering: A Thorough Investigation. https:\/\/doi.org\/10.48550\/arXiv.2305.12138","DOI":"10.48550\/arXiv.2305.12138"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","unstructured":"Hammond Pearce Baleegh Ahmad Benjamin Tan Brendan Dolan-Gavitt and Ramesh Karri. 2021. Asleep at the Keyboard? Assessing the Security of GitHub Copilot\u2019s Code Contributions. https:\/\/doi.org\/10.48550\/arXiv.2108.09293","DOI":"10.48550\/arXiv.2108.09293"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"crossref","unstructured":"Hammond Pearce Benjamin Tan Baleegh Ahmad Ramesh Karri and Brendan Dolan-Gavitt. 2022. Examining Zero-Shot Vulnerability Repair with Large Language Models. arxiv:2112.02125","DOI":"10.1109\/SP46215.2023.10179324"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"crossref","unstructured":"Neil Perry Megha Srivastava Deepak Kumar and Dan Boneh. 2022. Do Users Write More Insecure Code with AI Assistants?","DOI":"10.1145\/3576915.3623157"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISSREW51248.2020.00085"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3581641.3584037"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICMLA.2018.00120"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2688204.2688205"},{"key":"e_1_3_2_1_32_1","unstructured":"Gustavo Sandoval Hammond Pearce Teo Nys Ramesh Karri Siddharth Garg and Brendan Dolan-Gavitt. 2023. Lost at C: A User Study on the Security Implications of Large Language Model Code Assistants."},{"key":"e_1_3_2_1_33_1","unstructured":"Ilia Shumailov Zakhar Shumaylov Yiren Zhao Yarin Gal Nicolas Papernot and Ross Anderson. 2023. The Curse of Recursion: Training on Generated Data Makes Models Forget. arxiv:2305.17493"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.21227\/vp9n-wv96"},{"key":"e_1_3_2_1_35_1","unstructured":"Jovi Umawing. 2023. ChatGPT writes insecure code. https:\/\/www.malwarebytes.com\/blog\/news\/2023\/04\/chatgpt-creates-not-so-secure-code-study-finds"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/52.28119"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2201.11903"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2302.11382"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/2970276.2970326"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2306.02230"},{"key":"e_1_3_2_1_41_1","unstructured":"Shunyu Yao Dian Yu Jeffrey Zhao Izhak Shafran Thomas L. Griffiths Yuan Cao and Karthik Narasimhan. 2023. Tree of Thoughts: Deliberate Problem Solving with Large Language Models. arxiv:2305.10601"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236024.3236068"},{"key":"e_1_3_2_1_43_1","volume-title":"Devign: Effective Vulnerability Identification by Learning Comprehensive Program Semantics via Graph Neural Networks","author":"Zhou Yaqin","year":"2019","unstructured":"Yaqin Zhou, Shangqing Liu, Jingkai Siow, Xiaoning Du, and Yang Liu. 2019. Devign: Effective Vulnerability Identification by Learning Comprehensive Program Semantics via Graph Neural Networks. Curran Associates Inc., Red Hook, NY, USA. 10197\u201310207."}],"event":{"name":"PROMISE '23: 19th International Conference on Predictive Models and Data Analytics in Software Engineering","location":"San Francisco CA USA","acronym":"PROMISE '23","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering"]},"container-title":["Proceedings of the 19th International Conference on Predictive Models and Data Analytics in Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3617555.3617874","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3617555.3617874","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:45:58Z","timestamp":1750178758000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3617555.3617874"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,12,8]]},"references-count":42,"alternative-id":["10.1145\/3617555.3617874","10.1145\/3617555"],"URL":"https:\/\/doi.org\/10.1145\/3617555.3617874","relation":{},"subject":[],"published":{"date-parts":[[2023,12,8]]},"assertion":[{"value":"2023-12-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}