{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:58:54Z","timestamp":1750309134930,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":77,"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:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2024,9,11]]},"DOI":"10.1145\/3650212.3652110","type":"proceedings-article","created":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T11:44:25Z","timestamp":1726055065000},"page":"63-75","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Precise Compositional Buffer Overflow Detection via Heap Disjointness"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5985-6610","authenticated-orcid":false,"given":"Yiyuan","family":"Guo","sequence":"first","affiliation":[{"name":"The Hong Kong University of Science and Technology, Hong Kong, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0342-9518","authenticated-orcid":false,"given":"Peisen","family":"Yao","sequence":"additional","affiliation":[{"name":"Zhejiang University, Hangzhou, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6417-1034","authenticated-orcid":false,"given":"Charles","family":"Zhang","sequence":"additional","affiliation":[{"name":"The Hong Kong University of Science and Technology, Hong Kong, China"}]}],"member":"320","published-online":{"date-parts":[[2024,9,11]]},"reference":[{"volume-title":"The Clang Static Analyzer. https:\/\/clang-analyzer.llvm.org\/ Online","year":"2022","key":"e_1_3_2_1_1_1","unstructured":"2022. The Clang Static Analyzer. https:\/\/clang-analyzer.llvm.org\/ Online; accessed 28-July-2022."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1368088.1368118"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1646353.1646374"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462186"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276514"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/781131.781153"},{"key":"e_1_3_2_1_7_1","volume-title":"IKOS: A Framework for Static Analysis Based on Abstract Interpretation","author":"Brat Guillaume","year":"2014","unstructured":"Guillaume Brat, Jorge A. Navas, Nija Shi, and Arnaud Venet. 2014. IKOS: A Framework for Static Analysis Based on Abstract Interpretation. In Software Engineering and Formal Methods, Dimitra Giannakopoulou and Gwen Sala\u00fcn (Eds.). Springer International Publishing, Cham. 271\u2013277. isbn:978-3-319-10431-7"},{"key":"e_1_3_2_1_8_1","volume-title":"Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation (OSDI\u201908)","author":"Cadar Cristian","year":"2008","unstructured":"Cristian Cadar, Daniel Dunbar, and Dawson Engler. 2008. KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs. In Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation (OSDI\u201908). USENIX Association, USA. 209\u2013224."},{"key":"e_1_3_2_1_9_1","volume-title":"Infer: An Automatic Program Verifier for Memory Safety of C Programs","author":"Calcagno Cristiano","year":"2011","unstructured":"Cristiano Calcagno and Dino Distefano. 2011. Infer: An Automatic Program Verifier for Memory Safety of C Programs. In NASA Formal Methods, Mihaela Bobaru, Klaus Havelund, Gerard J. Holzmann, and Rajeev Joshi (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 459\u2013465. isbn:978-3-642-20398-5"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480917"},{"key":"e_1_3_2_1_11_1","volume-title":"International Static Analysis Symposium. 428\u2013449","author":"Chakraborty Supratik","year":"2017","unstructured":"Supratik Chakraborty, Ashutosh Gupta, and Divyesh Unadkat. 2017. Verifying array manipulating programs by tiling. In International Static Analysis Symposium. 428\u2013449."},{"volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Chalupa Marek","key":"e_1_3_2_1_12_1","unstructured":"Marek Chalupa, Vincent Mihalkovi\u010d, Anna \u0158echt\u00e1\u010dkov\u00e1, Luk\u00e1\u0161 Zaoral, and Jan Strej\u010dek. 2022. Symbiotic 9: String Analysis and Backward Symbolic Execution with Loop Folding. In Tools and Algorithms for the Construction and Analysis of Systems, Dana Fisman and Grigore Rosu (Eds.). Springer International Publishing, Cham. 462\u2013467. isbn:978-3-030-99527-0"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-88806-0_3"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.129.11"},{"key":"e_1_3_2_1_15_1","volume-title":"Necula","author":"Evan Chang Bor-Yuh","year":"2007","unstructured":"Bor-Yuh Evan Chang, Xavier Rival, and George C. Necula. 2007. Shape Analysis with Structural Invariant Checkers. In Static Analysis, Hanne Riis Nielson and Gilberto Fil\u00e9 (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 384\u2013401. isbn:978-3-540-74061-2"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292554"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1925844.1926399"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/512760.512770"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375615"},{"key":"e_1_3_2_1_21_1","first-page":"11956","volume-title":"Weak Updates. In Proceedings of the 19th European Conference on Programming Languages and Systems (ESOP\u201910)","author":"Dillig Isil","year":"2010","unstructured":"Isil Dillig, Thomas Dillig, and Alex Aiken. 2010. Fluid Updates: Beyond Strong vs. Weak Updates. In Proceedings of the 19th European Conference on Programming Languages and Systems (ESOP\u201910). Springer-Verlag, Berlin, Heidelberg. 246\u2013266. isbn:3-642-11956-5, 978-3-642-11956-9"},{"key":"e_1_3_2_1_22_1","volume-title":"Proceedings of the ACM International Conference on Object Oriented Programming Systems Languages and Applications (OOPSLA \u201910)","author":"Dillig Isil","year":"2010","unstructured":"Isil Dillig, Thomas Dillig, and Alex Aiken. 2010. Symbolic heap abstraction with demand-driven axiomatization of memory invariants. In Proceedings of the ACM International Conference on Object Oriented Programming Systems Languages and Applications (OOPSLA \u201910). ACM, New York, NY, USA. 397\u2013410. isbn:978-1-4503-0203-6"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993565"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3338112"},{"key":"e_1_3_2_1_25_1","volume-title":"Formal Verification of Object-Oriented Software","author":"F\u00e4hndrich Manuel","year":"1807","unstructured":"Manuel F\u00e4hndrich and Francesco Logozzo. 2011. Static Contract Checking with Abstract Interpretation. In Formal Verification of Object-Oriented Software, Bernhard Beckert and Claude March\u00e9 (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 10\u201330. isbn:978-3-642-18070-5"},{"volume-title":"Generic Combination of Heap and Value Analyses in Abstract Interpretation","author":"Ferrara Pietro","key":"e_1_3_2_1_26_1","unstructured":"Pietro Ferrara. 2014. Generic Combination of Heap and Value Analyses in Abstract Interpretation. In Verification, Model Checking, and Abstract Interpretation, Kenneth L. McMillan and Xavier Rival (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 302\u2013321. isbn:978-3-642-54013-4"},{"volume-title":"Modularly Combining Numeric Abstract Domains with Points-to Analysis, and a Scalable Static Numeric Analyzer for Java","author":"Zhoulai Fu.","key":"e_1_3_2_1_27_1","unstructured":"Zhoulai Fu. 2014. Modularly Combining Numeric Abstract Domains with Points-to Analysis, and a Scalable Static Numeric Analyzer for Java. In Verification, Model Checking, and Abstract Interpretation, Kenneth L. McMillan and Xavier Rival (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 282\u2013301. isbn:978-3-642-54013-4"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/948109.948155"},{"key":"e_1_3_2_1_29_1","volume-title":"Dill","author":"Ganesh Vijay","year":"2007","unstructured":"Vijay Ganesh and David L. Dill. 2007. A Decision Procedure for Bit-Vectors and Arrays. In Computer Aided Verification, Werner Damm and Holger Hermanns (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 519\u2013531. isbn:978-3-540-73368-3"},{"key":"e_1_3_2_1_30_1","volume-title":"Navas","author":"Garcia-Contreras Isabel","year":"2022","unstructured":"Isabel Garcia-Contreras, Arie Gurfinkel, and Jorge A. Navas. 2022. Efficient Modular SMT-Based Model Checking of Pointer Programs. In Static Analysis, Gagandeep Singh and Caterina Urban (Eds.). Springer Nature Switzerland, Cham. 227\u2013246. isbn:978-3-031-22308-2"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040333"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290370"},{"key":"e_1_3_2_1_33_1","volume-title":"International Static Analysis Symposium. 188\u2013204","author":"Gulavani Bhargav S","year":"2009","unstructured":"Bhargav S Gulavani, Supratik Chakraborty, Ganesan Ramalingam, and Aditya V Nori. 2009. Bottom-up shape analysis. In International Static Analysis Symposium. 188\u2013204."},{"key":"e_1_3_2_1_34_1","volume-title":"Navas","author":"Gurfinkel Arie","year":"2015","unstructured":"Arie Gurfinkel, Temesghen Kahsai, Anvesh Komuravelli, and Jorge A. Navas. 2015. The SeaHorn Verification Framework. In Computer Aided Verification, Daniel Kroening and Corina S. P\u0103s\u0103reanu (Eds.). Springer International Publishing, Cham. 343\u2013361. isbn:978-3-319-21690-4"},{"volume-title":"Engineering Secure and Dependable Software Systems","author":"Gurfinkel Arie","key":"e_1_3_2_1_35_1","unstructured":"Arie Gurfinkel and Jorge A Navas. 2019. Automatic Program Verification with SEAHORN. In Engineering Secure and Dependable Software Systems. IOS Press, 83\u2013111."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375623"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2931098"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.5555\/1765871.1765924"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3230624"},{"key":"e_1_3_2_1_40_1","unstructured":"Yoonseok Ko and Hakjoo Oh. 2023. Learning to Boost Disjunctive Static Bug-Finders."},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2015.7542257"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1109\/CGO.2004.1281665"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/1273442.1250766"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3527325"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/1453101.1453137"},{"key":"e_1_3_2_1_46_1","volume-title":"FOOL 2012: 19th International Workshop on Foundations of Object-Oriented Languages. 96","author":"Lee Hongki","year":"2012","unstructured":"Hongki Lee, Sooncheol Won, Joonho Jin, Junhee Cho, and Sukyoung Ryu. 2012. SAFE: Formal specification and implementation of a scalable analysis framework for ECMAScript. In FOOL 2012: 19th International Workshop on Foundations of Object-Oriented Languages. 96."},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3093333.3009881"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/1882291.1882338"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/2025113.2025160"},{"key":"e_1_3_2_1_50_1","volume-title":"International Workshop on Verification, Model Checking, and Abstract Interpretation. 282\u2013299","author":"Liu Jiangchao","year":"2015","unstructured":"Jiangchao Liu and Xavier Rival. 2015. Abstraction of arrays based on non contiguous partitions. In International Workshop on Verification, Model Checking, and Abstract Interpretation. 282\u2013299."},{"key":"e_1_3_2_1_51_1","volume-title":"Proceedings of the 9th European software engineering conference held jointly with 11th ACM SIGSOFT international symposium on Foundations of software engineering. 317\u2013326","author":"Benjamin Livshits V","year":"2003","unstructured":"V Benjamin Livshits and Monica S Lam. 2003. Tracking pointers with path and context sensitivity for bug detection in C programs. In Proceedings of the 9th European software engineering conference held jointly with 11th ACM SIGSOFT international symposium on Foundations of software engineering. 317\u2013326."},{"volume-title":"Statically Inferring Complex Heap, Array, and Numeric Invariants","author":"McCloskey Bill","key":"e_1_3_2_1_52_1","unstructured":"Bill McCloskey, Thomas Reps, and Mooly Sagiv. 2010. Statically Inferring Complex Heap, Array, and Numeric Invariants. In Static Analysis, Radhia Cousot and Matthieu Martel (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 71\u201399. isbn:978-3-642-15769-1"},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254092"},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371078"},{"key":"e_1_3_2_1_55_1","volume-title":"OpenSSL Security Advisory [01","author":"SSL.","year":"2022","unstructured":"OpenSSL. 2022. OpenSSL Security Advisory [01 November 2022]. https:\/\/www.openssl.org\/news\/secadv\/20221101.txt Online; accessed 7-Nov-2022."},{"key":"e_1_3_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/3092703.3092728"},{"key":"e_1_3_2_1_57_1","volume-title":"SMACK: Decoupling Source Language Details from Verifier Implementations","author":"Rakamari\u0107 Zvonimir","year":"2014","unstructured":"Zvonimir Rakamari\u0107 and Michael Emmi. 2014. SMACK: Decoupling Source Language Details from Verifier Implementations. In Computer Aided Verification, Armin Biere and Roderick Bloem (Eds.). Springer International Publishing, Cham. 106\u2013113. isbn:978-3-319-08867-9"},{"key":"e_1_3_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_3_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/1275497.1275501"},{"key":"e_1_3_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/271510.271517"},{"key":"e_1_3_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/514188.514190"},{"volume-title":"OSS-Fuzz - Google","author":"Serebryany Kostya","key":"e_1_3_2_1_62_1","unstructured":"Kostya Serebryany. 2017. OSS-Fuzz - Google\u2019 s continuous fuzzing service for open source software. USENIX Association, Vancouver, BC."},{"key":"e_1_3_2_1_63_1","volume-title":"Two approaches to interprocedural data flow analysis. New York Univ. Comput. Sci","author":"Sharir M","year":"2011","unstructured":"M Sharir and A Pnueli. 1978. Two approaches to interprocedural data flow analysis. New York Univ. Comput. Sci. Dept., New York, NY. https:\/\/cds.cern.ch\/record\/120118"},{"key":"e_1_3_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192418"},{"key":"e_1_3_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/3460319.3464826"},{"key":"e_1_3_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1561\/2500000014"},{"key":"e_1_3_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/1133981.1134027"},{"key":"e_1_3_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360566"},{"key":"e_1_3_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/2338965.2336784"},{"volume-title":"The heartbleed bug. https:\/\/heartbleed.com\/ Online","year":"2022","key":"e_1_3_2_1_70_1","unstructured":"Synopsys. 2020. The heartbleed bug. https:\/\/heartbleed.com\/ Online; accessed 7-Nov-2022."},{"key":"e_1_3_2_1_71_1","first-page":"0","article-title":"A first step towards automated detection of buffer overrun vulnerabilities","volume":"20","author":"Wagner David A","year":"2000","unstructured":"David A Wagner, Jeffrey S Foster, Eric A Brewer, and Alexander Aiken. 2000. A first step towards automated detection of buffer overrun vulnerabilities.. In NDSS. 20, 0.","journal-title":"NDSS."},{"key":"e_1_3_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1145\/223428.207111"},{"key":"e_1_3_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040334"},{"key":"e_1_3_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040334"},{"key":"e_1_3_2_1_75_1","doi-asserted-by":"publisher","DOI":"10.1145\/940071.940115"},{"key":"e_1_3_2_1_76_1","volume-title":"Proceedings of the 2008 international symposium on Software testing and analysis. 225\u2013236","author":"Xu Guoqing","year":"2008","unstructured":"Guoqing Xu and Atanas Rountev. 2008. Merging equivalent contexts for scalable heap-cloning-based context-sensitive points-to analysis. In Proceedings of the 2008 international symposium on Software testing and analysis. 225\u2013236."},{"key":"e_1_3_2_1_77_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192416"}],"event":{"name":"ISSTA '24: 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering","AITO"],"location":"Vienna Austria","acronym":"ISSTA '24"},"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.3652110","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3650212.3652110","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T22:50:06Z","timestamp":1750287006000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3650212.3652110"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,9,11]]},"references-count":77,"alternative-id":["10.1145\/3650212.3652110","10.1145\/3650212"],"URL":"https:\/\/doi.org\/10.1145\/3650212.3652110","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"}}]}}