{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,2]],"date-time":"2025-08-02T19:02:07Z","timestamp":1754161327210,"version":"3.41.2"},"publisher-location":"New York, NY, USA","reference-count":30,"publisher":"ACM","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2025,6,23]]},"DOI":"10.1145\/3696630.3728581","type":"proceedings-article","created":{"date-parts":[[2025,7,28]],"date-time":"2025-07-28T19:09:27Z","timestamp":1753729767000},"page":"1060-1064","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["VO-GCSE: Verification Optimization through Global Common Subexpression Elimination"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6102-4343","authenticated-orcid":false,"given":"Rafael S\u00e1","family":"Menezes","sequence":"first","affiliation":[{"name":"University of Manchester, Manchester, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9002-5935","authenticated-orcid":false,"given":"Norbert","family":"Tihanyi","sequence":"additional","affiliation":[{"name":"Technology Innovation Institute, Abu Dhabi, United Arab Emirates"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6102-7114","authenticated-orcid":false,"given":"Ridhi","family":"Jain","sequence":"additional","affiliation":[{"name":"Technology Innovation Institute, Abu Dhabi, United Arab Emirates"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-2654-1251","authenticated-orcid":false,"given":"Alexander","family":"Levin","sequence":"additional","affiliation":[{"name":"Nvidia, Haifa, Israel"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7608-2052","authenticated-orcid":false,"given":"Rosiane","family":"de Freitas","sequence":"additional","affiliation":[{"name":"Federal University of Amazonas, Manaus, Brazil"}],"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"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,7,28]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"2024. https:\/\/github.com\/esbmc\/esbmc\/releases\/tag\/v7.8.1. Accessed: 2025-01-13."},{"key":"e_1_3_2_1_2_1","unstructured":"2024. https:\/\/raw.githubusercontent.com\/esbmc\/esbmc\/refs\/heads\/master\/docs\/examples\/GCSE_real_example.c. Accessed: 2025-01-13."},{"key":"e_1_3_2_1_3_1","unstructured":"Aho Alfred V Lam Monica S Sethi Ravi Ullman Jeffrey D et al. 2007. Compilers-principles techniques and tools. pearson Education."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/197405.197406"},{"volume-title":"The cyber security body of knowledge","author":"Basin David","key":"e_1_3_2_1_5_1","unstructured":"David Basin. 2021. The cyber security body of knowledge. University of Bristol, ch. Formal Methods for Security, version..[Online ...."},{"key":"e_1_3_2_1_6_1","volume-title":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 887\u2013904","author":"Beyer Dirk","year":"2016","unstructured":"Dirk Beyer. 2016. Reliable and reproducible competition results with benchexec and witnesses (report on SV-COMP 2016). In International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 887\u2013904."},{"key":"e_1_3_2_1_7_1","volume-title":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 495\u2013522","author":"Beyer Dirk","year":"2023","unstructured":"Dirk Beyer. 2023. Competition on software verification and witness validation: SV-COMP 2023. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 495\u2013522."},{"key":"e_1_3_2_1_8_1","volume-title":"Bounded model checking using satisfiability solving. Formal methods in system design 19","author":"Clarke Edmund","year":"2001","unstructured":"Edmund Clarke, Armin Biere, Richard Raimi, and Yunshan Zhu. 2001. Bounded model checking using satisfiability solving. Formal methods in system design 19 (2001), 7\u201334."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/390013.808480"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/B0-12-227410-5\/00126-5"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/504709.504710"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"crossref","first-page":"957","DOI":"10.1109\/TSE.2011.59","article-title":"SMT-based bounded model checking for embedded ANSI-C software","volume":"38","author":"Cordeiro Lucas","year":"2011","unstructured":"Lucas Cordeiro, Bernd Fischer, and Joao Marques-Silva. 2011. SMT-based bounded model checking for embedded ANSI-C software. IEEE Transactions on Software Engineering 38, 4 (2011), 957\u2013974.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"e_1_3_2_1_13_1","volume-title":"Proceedings of the 33rd International Conference on Software Engineering, ICSE 2011","author":"Lucas","year":"2011","unstructured":"Lucas C. Cordeiro and Bernd Fischer. 2011. Verifying multi-threaded software using smt-based context-bounded model checking. In Proceedings of the 33rd International Conference on Software Engineering, ICSE 2011, Waikiki, Honolulu, HI, USA, May 21\u201328, 2011, Richard N. Taylor, Harald C. Gall, and Nenad Medvidovic (Eds.). ACM, 331\u2013340."},{"volume-title":"Principles of Abstract Interpretation","author":"Cousot Patrick","key":"e_1_3_2_1_14_1","unstructured":"Patrick Cousot. 2021. Principles of Abstract Interpretation. MIT Press."},{"key":"e_1_3_2_1_15_1","volume-title":"Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages. 238\u2013252","author":"Cousot Patrick","year":"1977","unstructured":"Patrick Cousot and Radhia Cousot. 1977. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fix-points. In Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages. 238\u2013252."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/2506375","article-title":"Loop invariants: Analysis, classification, and examples","volume":"46","author":"Furia Carlo A","year":"2014","unstructured":"Carlo A Furia, Bertrand Meyer, and Sergey Velder. 2014. Loop invariants: Analysis, classification, and examples. ACM Computing Surveys (CSUR) 46, 3 (2014), 1\u201351.","journal-title":"ACM Computing Surveys (CSUR)"},{"key":"e_1_3_2_1_17_1","unstructured":"Mikhail R. Gadelha Felipe R. Monteiro Jeremy Morse Lucas C. Cordeiro Bernd Fischer and Denis A. Nicole. [n. d.]. ESBMC: 5.0: An Industrial-Strength Model Checker. https:\/\/github.com\/esbmc\/esbmc"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"crossref","first-page":"519","DOI":"10.1137\/0204044","article-title":"A simple algorithm for global data flow analysis problems","volume":"4","author":"Hecht Matthew S","year":"1975","unstructured":"Matthew S Hecht and Jeffrey D Ullman. 1975. A simple algorithm for global data flow analysis problems. SIAM J. Comput. 4, 4 (1975), 519\u2013532.","journal-title":"SIAM J. Comput."},{"key":"e_1_3_2_1_19_1","volume-title":"Proceedings of the 1st Annual ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages","author":"Kildall Gary A.","year":"1973","unstructured":"Gary A. Kildall. 1973. A Unified Approach to Global Program Optimization. In Proceedings of the 1st Annual ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (Boston, Massachusetts) (POPL '73). Association for Computing Machinery, New York, NY, USA, 194\u2013206. 10.1145\/512927.512945"},{"volume-title":"Decision procedures","author":"Kroening Daniel","key":"e_1_3_2_1_20_1","unstructured":"Daniel Kroening and Ofer Strichman. 2016. Decision procedures. Springer."},{"key":"e_1_3_2_1_21_1","volume-title":"International Symposium on Code Generation and Optimization, 2004. CGO 2004. 75\u201386","author":"Lattner C.","year":"2004","unstructured":"C. Lattner and V. Adve. 2004. LLVM: a compilation framework for lifelong program analysis & transformation. In International Symposium on Code Generation and Optimization, 2004. CGO 2004. 75\u201386. 10.1109\/CGO.2004.1281665"},{"key":"e_1_3_2_1_22_1","volume-title":"Proceedings of the 31st ACM SIGSOFT International Symposium on Software Testing and Analysis. 777\u2013780","author":"Menezes Rafael","year":"2022","unstructured":"Rafael Menezes, Daniel Moura, Helena Cavalcante, Rosiane de Freitas, and Lucas C Cordeiro. 2022. ESBMC-Jimple: verifying Kotlin programs via jimple intermediate representation. In Proceedings of the 31st ACM SIGSOFT International Symposium on Software Testing and Analysis. 777\u2013780."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-57256-2_24"},{"key":"e_1_3_2_1_24_1","volume-title":"Cordeiro","author":"Monteiro Felipe R.","year":"2022","unstructured":"Felipe R. Monteiro, Mikhail R. Gadelha, and Lucas C. Cordeiro. 2022. Model checking C++ programs. Softw. Test. Verification Reliab. 32, 1 (2022)."},{"key":"e_1_3_2_1_25_1","volume-title":"Proceedings of the ACM Annual Conference","author":"Schneck Paul B.","year":"1973","unstructured":"Paul B. Schneck. 1973. A Survey of Compiler Optimization Techniques. In Proceedings of the ACM Annual Conference (Atlanta, Georgia, USA) (ACM '73). Association for Computing Machinery, New York, NY, USA, 106\u2013113. 10.1145\/800192.805690"},{"key":"e_1_3_2_1_26_1","volume-title":"Computer Aided Verification: 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14\u201320, 2011. Proceedings 23","author":"Sharma Rahul","year":"2011","unstructured":"Rahul Sharma, Isil Dillig, Thomas Dillig, and Alex Aiken. 2011. Simplifying loop invariant generation using splitter predicates. In Computer Aided Verification: 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14\u201320, 2011. Proceedings 23. Springer, 703\u2013719."},{"key":"e_1_3_2_1_27_1","volume-title":"Proceedings of the 27th ACM International Conference on Architectural Support for Programming Languages and Operating Systems","author":"Theodoridis Theodoros","year":"2022","unstructured":"Theodoros Theodoridis, Tobias Grosser, and Zhendong Su. 2022. Understanding and exploiting optimal function inlining. In Proceedings of the 27th ACM International Conference on Architectural Support for Programming Languages and Operating Systems (Lausanne, Switzerland) (ASPLOS '22). Association for Computing Machinery, New York, NY, USA, 977\u2013989. 10.1145\/3503222.3507744"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10664-024-10590-1"},{"key":"e_1_3_2_1_29_1","volume-title":"Proceedings of the 19th International Conference on Predictive Models and Data Analytics in Software Engineering","author":"Tihanyi Norbert","year":"2023","unstructured":"Norbert Tihanyi, Tamas Bisztray, Ridhi Jain, Mohamed Amine Ferrag, Lucas C. Cordeiro, and Vasileios Mavroeidis. 2023. The FormAI Dataset: Generative AI in Software Security through the Lens of Formal Verification. In Proceedings of the 19th International Conference on Predictive Models and Data Analytics in Software Engineering (San Francisco, CA, USA) (PROMISE 2023). Association for Computing Machinery, New York, NY, USA, 33\u201343. 10.1145\/3617555.3617874"},{"key":"e_1_3_2_1_30_1","volume-title":"Cordeiro","author":"Wu Tong","year":"2024","unstructured":"Tong Wu, Shale Xiong, Edoardo Manino, Gareth Stockwell, and Lucas C. Cordeiro. 2024. Verifying components of Arm\u00ae Confidential Computing Architecture with ESBMC. arXiv preprint arXiv:2406.04375 (2024). https:\/\/arxiv.org\/abs\/2406.04375 Accessed: 2024-11-19."}],"event":{"name":"FSE Companion '25: 33rd ACM International Conference on the Foundations of Software Engineering","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering"],"location":"Clarion Hotel Trondheim Trondheim Norway","acronym":"FSE Companion '25"},"container-title":["Proceedings of the 33rd ACM International Conference on the Foundations of Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3696630.3728581","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,28]],"date-time":"2025-07-28T19:18:28Z","timestamp":1753730308000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3696630.3728581"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6,23]]},"references-count":30,"alternative-id":["10.1145\/3696630.3728581","10.1145\/3696630"],"URL":"https:\/\/doi.org\/10.1145\/3696630.3728581","relation":{},"subject":[],"published":{"date-parts":[[2025,6,23]]},"assertion":[{"value":"2025-07-28","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}