{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,22]],"date-time":"2026-01-22T19:03:16Z","timestamp":1769108596650,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":25,"publisher":"ACM","license":[{"start":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T00:00:00Z","timestamp":1726012800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"Ethereum Foundation","award":["FY22-0751"],"award-info":[{"award-number":["FY22-0751"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2024,9,11]]},"DOI":"10.1145\/3650212.3685304","type":"proceedings-article","created":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T11:44:25Z","timestamp":1726055065000},"page":"1836-1840","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["ESBMC-Python: A Bounded Model Checker for Python Programs"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0002-5124-8607","authenticated-orcid":false,"given":"Bruno","family":"Farias","sequence":"first","affiliation":[{"name":"University of Manchester, Manchester, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6102-4343","authenticated-orcid":false,"given":"Rafael","family":"Menezes","sequence":"additional","affiliation":[{"name":"University of Manchester, Manchester, United Kingdom \/ Federal University of Amazonas, Manaus, Brazil"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2758-4638","authenticated-orcid":false,"given":"Eddie B.","family":"de Lima Filho","sequence":"additional","affiliation":[{"name":"TPV Technology, Manaus, Brazil"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1893-6259","authenticated-orcid":false,"given":"Youcheng","family":"Sun","sequence":"additional","affiliation":[{"name":"University of Manchester, Manchester, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6235-4272","authenticated-orcid":false,"given":"Lucas C.","family":"Cordeiro","sequence":"additional","affiliation":[{"name":"University of Manchester, Manchester, United Kingdom \/ Federal University of Amazonas, Manaus, Brazil"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,9,11]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Proceedings of the 12th USENIX Conference on Operating Systems Design and Implementation (OSDI\u201916)","author":"Abadi Mart\u00edn","year":"2016","unstructured":"Mart\u00edn Abadi, Paul Barham, Jianmin Chen, Zhifeng Chen, Andy Davis, Jeffrey Dean, Matthieu Devin, Sanjay Ghemawat, Geoffrey Irving, Michael Isard, Manjunath Kudlur, Josh Levenberg, Rajat Monga, Sherry Moore, Derek G. Murray, Benoit Steiner, Paul Tucker, Vijay Vasudevan, Pete Warden, Martin Wicke, Yuan Yu, and Xiaoqiang Zheng. 2016. TensorFlow: a system for large-scale machine learning. In Proceedings of the 12th USENIX Conference on Operating Systems Design and Implementation (OSDI\u201916). USENIX Association, USA. 265\u2013283. isbn:9781931971331"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1186\/s13173-016-0041-8"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/SBESC.2014.14"},{"key":"e_1_3_2_1_4_1","volume-title":"Handbook of satisfiability","author":"Biere Armin","unstructured":"Armin Biere. 2021. Bounded model checking. In Handbook of satisfiability. IOS press, 739\u2013764."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99524-9_9"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/TR.2018.2873260"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2019.03.015"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2011.59"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/115372.115320"},{"key":"e_1_3_2_1_10_1","volume-title":"Thales Araujo da Silva, and Lucas C Cordeiro.","author":"de Sousa Janislley Oliveira","year":"2023","unstructured":"Janislley Oliveira de Sousa, Bruno Carvalho de Farias, Thales Araujo da Silva, and Lucas C Cordeiro. 2023. Finding Software Vulnerabilities in Open-Source C Projects via Bounded Model Checking. arXiv preprint arXiv:2311.05281."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(95)00007-0"},{"key":"e_1_3_2_1_12_1","volume-title":"Deep learning with Python. 1","author":"Ketkar Nikhil","unstructured":"Nikhil Ketkar and Eder Santana. 2017. Deep learning with Python. 1, Springer."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_26"},{"key":"e_1_3_2_1_14_1","unstructured":"Magnus Madsen. 2015. Static analysis of dynamic languages."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3533767.3543294"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1002\/stvr.1793"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3127360.3127367"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.3233\/sat190101"},{"key":"e_1_3_2_1_19_1","volume-title":"PyTorch: an imperative style, high-performance deep learning library","author":"Paszke Adam","unstructured":"Adam Paszke, Sam Gross, Francisco Massa, Adam Lerer, James Bradbury, Gregory Chanan, Trevor Killeen, Zeming Lin, Natalia Gimelshein, Luca Antiga, Alban Desmaison, Andreas K\u00f6pf, Edward Yang, Zach DeVito, Martin Raison, Alykhan Tejani, Sasank Chilamkurthy, Benoit Steiner, Lu Fang, Junjie Bai, and Soumith Chintala. 2019. PyTorch: an imperative style, high-performance deep learning library. Curran Associates Inc., Red Hook, NY, USA."},{"key":"e_1_3_2_1_20_1","unstructured":"Laurent Peuch. 2024. ast2json. https:\/\/pypi.org\/project\/ast2json\/ Accessed: 2024-06-03"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2693208.2693240"},{"key":"e_1_3_2_1_22_1","unstructured":"Python Software Foundation. 2024. ast - Abstract Syntax Trees. https:\/\/docs.python.org\/3\/library\/ast.html Accessed: 2024-06-03"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-41418-4_15"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3510454.3516855"},{"key":"e_1_3_2_1_25_1","unstructured":"Guido Van Rossum and Fred L Drake Jr. 1995. Python tutorial."}],"event":{"name":"ISSTA '24: 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis","location":"Vienna Austria","acronym":"ISSTA '24","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering","AITO"]},"container-title":["Proceedings of the 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3650212.3685304","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3650212.3685304","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T00:58:09Z","timestamp":1750294689000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3650212.3685304"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,9,11]]},"references-count":25,"alternative-id":["10.1145\/3650212.3685304","10.1145\/3650212"],"URL":"https:\/\/doi.org\/10.1145\/3650212.3685304","relation":{},"subject":[],"published":{"date-parts":[[2024,9,11]]},"assertion":[{"value":"2024-09-11","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}