{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,13]],"date-time":"2026-04-13T14:57:05Z","timestamp":1776092225391,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":51,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,11,8]],"date-time":"2020-11-08T00:00:00Z","timestamp":1604793600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"ISF","award":["1996\/18"],"award-info":[{"award-number":["1996\/18"]}]},{"DOI":"10.13039\/100011199","name":"European Research Council","doi-asserted-by":"publisher","award":["819141"],"award-info":[{"award-number":["819141"]}],"id":[{"id":"10.13039\/100011199","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2020,11,8]]},"DOI":"10.1145\/3368089.3409698","type":"proceedings-article","created":{"date-parts":[[2020,11,8]],"date-time":"2020-11-08T06:03:52Z","timestamp":1604815432000},"page":"197-208","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["Past-sensitive pointer analysis for symbolic execution"],"prefix":"10.1145","author":[{"given":"David","family":"Trabish","sequence":"first","affiliation":[{"name":"Tel Aviv University, Israel"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Timotej","family":"Kapus","sequence":"additional","affiliation":[{"name":"Imperial College London, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Noam","family":"Rinetzky","sequence":"additional","affiliation":[{"name":"Tel Aviv University, Israel"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Cristian","family":"Cadar","sequence":"additional","affiliation":[{"name":"Imperial College London, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2020,11,8]]},"reference":[{"key":"e_1_3_2_2_1_1","volume-title":"Ullman","author":"Aho Alfred V.","year":"2006","unstructured":"Alfred V. Aho , Monica S. Lam , Ravi Sethi , and Jefrey D . Ullman . 2006 . Compilers : Principles, Techniques, and Tools (2nd ed.). Addison Wesley . Alfred V. Aho, Monica S. Lam, Ravi Sethi, and Jefrey D. Ullman. 2006. Compilers: Principles, Techniques, and Tools (2nd ed.). Addison Wesley."},{"key":"e_1_3_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2008.30"},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-008-0090-1"},{"key":"e_1_3_2_2_5_1","volume-title":"Proc. of the International Symposium on Software Testing and Analysis (ISSTA'08)","author":"Beckman Nels E.","unstructured":"Nels E. Beckman , Aditya V. Nori , Sriram K. Rajamani , and Robert J. Simmons . 2008. Proofs from tests . In Proc. of the International Symposium on Software Testing and Analysis (ISSTA'08) (Seattle, WA, USA). Nels E. Beckman, Aditya V. Nori, Sriram K. Rajamani, and Robert J. Simmons. 2008. Proofs from tests. In Proc. of the International Symposium on Software Testing and Analysis (ISSTA'08) (Seattle, WA, USA)."},{"key":"e_1_3_2_2_6_1","volume-title":"Levitt","author":"Boyer Robert S.","year":"1975","unstructured":"Robert S. Boyer , Bernard Elspas , and Karl N . Levitt . 1975 . SELECT-A formal system for testing and debugging programs by symbolic execution. ACM SIGPLAN Notices 10, 6 ( 1975 ), 234-245. Robert S. Boyer, Bernard Elspas, and Karl N. Levitt. 1975. SELECT-A formal system for testing and debugging programs by symbolic execution. ACM SIGPLAN Notices 10, 6 ( 1975 ), 234-245."},{"key":"e_1_3_2_2_8_1","volume-title":"Proc. of the 8th USENIX Symposium on Operating Systems Design and Implementation (OSDI'08)","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 Proc. of the 8th USENIX Symposium on Operating Systems Design and Implementation (OSDI'08) (San Diego, CA, USA). Cristian Cadar, Daniel Dunbar, and Dawson Engler. 2008. KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs. In Proc. of the 8th USENIX Symposium on Operating Systems Design and Implementation (OSDI'08) (San Diego, CA, USA)."},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/11537328_2"},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1180405.1180445"},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1455518.1455522"},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"crossref","unstructured":"Cristian Cadar and Koushik Sen. 2013. Symbolic Execution for Software Testing: Three Decades Later. Communications of the Association for Computing Machinery (CACM) 56 2 ( 2013 ) 82-90.  Cristian Cadar and Koushik Sen. 2013. Symbolic Execution for Software Testing: Three Decades Later. Communications of the Association for Computing Machinery (CACM) 56 2 ( 2013 ) 82-90.","DOI":"10.1145\/2408776.2408795"},{"key":"e_1_3_2_2_13_1","volume-title":"Proc. of the 7th USENIX Symposium on Operating Systems Design and Implementation (OSDI'06)","author":"Castro Miguel","year":"2006","unstructured":"Miguel Castro , Manuel Costa , and Tim Harris . 2006 . Securing Software by Enforcing Data-flow Integrity . In Proc. of the 7th USENIX Symposium on Operating Systems Design and Implementation (OSDI'06) (Seattle, WA, USA). Miguel Castro, Manuel Costa, and Tim Harris. 2006. Securing Software by Enforcing Data-flow Integrity. In Proc. of the 7th USENIX Symposium on Operating Systems Design and Implementation (OSDI'06) (Seattle, WA, USA)."},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2012.31"},{"key":"e_1_3_2_2_15_1","volume-title":"Proc. of the 26th ACM Symposium on the Principles of Programming Languages (POPL'99)","author":"Chatterjee Ramkrishna","unstructured":"Ramkrishna Chatterjee , Barbara G. Ryder , and William A. Landi . 1999. Relevant Context Inference . In Proc. of the 26th ACM Symposium on the Principles of Programming Languages (POPL'99) (San Antonio, TX, USA). Ramkrishna Chatterjee, Barbara G. Ryder, and William A. Landi. 1999. Relevant Context Inference. In Proc. of the 26th ACM Symposium on the Principles of Programming Languages (POPL'99) (San Antonio, TX, USA)."},{"key":"e_1_3_2_2_16_1","volume-title":"Proc. of the Conference on Programing Language Design and Implementation (PLDI'00)","author":"Cheng Ben-Chung","unstructured":"Ben-Chung Cheng and Wen-Mei W. Hwu . 2000. Modular Interprocedural Pointer Analysis Using Access Paths: Design, Implementation, and Evaluation . In Proc. of the Conference on Programing Language Design and Implementation (PLDI'00) (Vancouver, BC, Canada). Ben-Chung Cheng and Wen-Mei W. Hwu. 2000. Modular Interprocedural Pointer Analysis Using Access Paths: Design, Implementation, and Evaluation. In Proc. of the Conference on Programing Language Design and Implementation (PLDI'00) (Vancouver, BC, Canada)."},{"key":"e_1_3_2_2_17_1","volume-title":"Proc. of the 28th International Conference on Software Engineering (ICSE'06)","author":"Christakis Maria","year":"2006","unstructured":"Maria Christakis , Peter M\u00fcller , and Valentin W\u00fcstholz . 2006 . Guiding Dynamic Symbolic Execution Toward Unverified Program Executions . In Proc. of the 28th International Conference on Software Engineering (ICSE'06) (Shanghai, China). Maria Christakis, Peter M\u00fcller, and Valentin W\u00fcstholz. 2006. Guiding Dynamic Symbolic Execution Toward Unverified Program Executions. In Proc. of the 28th International Conference on Software Engineering (ICSE'06) (Shanghai, China)."},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/800191.805647"},{"key":"e_1_3_2_2_19_1","volume-title":"Proc. of the 6th European Conference on Computer Systems (EuroSys'11)","author":"Collingbourne Peter","unstructured":"Peter Collingbourne , Cristian Cadar , and Paul H.J. Kelly . 2011. Symbolic Crosschecking of Floating-Point and SIMD Code . In Proc. of the 6th European Conference on Computer Systems (EuroSys'11) (Salzburg, Austria). Peter Collingbourne, Cristian Cadar, and Paul H.J. Kelly. 2011. Symbolic Crosschecking of Floating-Point and SIMD Code. In Proc. of the 6th European Conference on Computer Systems (EuroSys'11) (Salzburg, Austria)."},{"key":"e_1_3_2_2_20_1","volume-title":"Proc. of the Haifa Verification Conference (HVC'11)","author":"Collingbourne Peter","unstructured":"Peter Collingbourne , Cristian Cadar , and Paul H.J. Kelly . 2011. Symbolic Testing of OpenCL Code . In Proc. of the Haifa Verification Conference (HVC'11) (Haifa, Israel). Peter Collingbourne, Cristian Cadar, and Paul H.J. Kelly. 2011. Symbolic Testing of OpenCL Code. In Proc. of the Haifa Verification Conference (HVC'11) (Haifa, Israel)."},{"key":"e_1_3_2_2_21_1","volume-title":"Proc. of the 4th ACM Symposium on the Principles of Programming Languages (POPL'77)","author":"Cousot P.","unstructured":"P. Cousot and R. Cousot . 1977. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints . In Proc. of the 4th ACM Symposium on the Principles of Programming Languages (POPL'77) (Los Angeles, CA, USA). P. Cousot and R. Cousot. 1977. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In Proc. of the 4th ACM Symposium on the Principles of Programming Languages (POPL'77) (Los Angeles, CA, USA)."},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1062455.1062533"},{"key":"e_1_3_2_2_23_1","first-page":"9","article-title":"Satisfiability modulo theories: introduction and applications","volume":"54","author":"Moura Leonardo De","year":"2011","unstructured":"Leonardo De Moura and Nikolaj Bj\u00f8rner . 2011 . Satisfiability modulo theories: introduction and applications . Communications of the Association for Computing Machinery (CACM) 54 , 9 (Sept. 2011 ), 69-77. Leonardo De Moura and Nikolaj Bj\u00f8rner. 2011. Satisfiability modulo theories: introduction and applications. Communications of the Association for Computing Machinery (CACM) 54, 9 (Sept. 2011 ), 69-77.","journal-title":"Communications of the Association for Computing Machinery (CACM)"},{"key":"e_1_3_2_2_24_1","volume-title":"Proc. of the International Symposium on Software Testing and Analysis (ISSTA'09)","author":"Elkarablieh Bassem","unstructured":"Bassem Elkarablieh , Patrice Godefroid , and Michael Y. Levin . 2009. Precise Pointer Reasoning for Dynamic Test Generation . In Proc. of the International Symposium on Software Testing and Analysis (ISSTA'09) (Chicago, IL, USA). Bassem Elkarablieh, Patrice Godefroid, and Michael Y. Levin. 2009. Precise Pointer Reasoning for Dynamic Test Generation. In Proc. of the International Symposium on Software Testing and Analysis (ISSTA'09) (Chicago, IL, USA)."},{"key":"e_1_3_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065036"},{"key":"e_1_3_2_2_26_1","volume-title":"Proc. of the 15th Network and Distributed System Security Symposium (NDSS'08)","author":"Godefroid Patrice","unstructured":"Patrice Godefroid , Michael Y. Levin , and David A. Molnar . 2008. Automated Whitebox Fuzz Testing . In Proc. of the 15th Network and Distributed System Security Symposium (NDSS'08) (San Diego, CA, USA). Patrice Godefroid, Michael Y. Levin, and David A. Molnar. 2008. Automated Whitebox Fuzz Testing. In Proc. of the 15th Network and Distributed System Security Symposium (NDSS'08) (San Diego, CA, USA)."},{"key":"e_1_3_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706307"},{"key":"e_1_3_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133892"},{"key":"e_1_3_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3213846.3213860"},{"key":"e_1_3_2_2_30_1","volume-title":"Proc. of the ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE'06)","author":"Gulavani Bhargav S.","unstructured":"Bhargav S. Gulavani , Thomas A. Henzinger , Yamini Kannan , Aditya V. Nori , and Sriram K. Rajamani . 2006. Synergy: A New Algorithm for Property Checking . In Proc. of the ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE'06) (Graz, Austria). Bhargav S. Gulavani, Thomas A. Henzinger, Yamini Kannan, Aditya V. Nori, and Sriram K. Rajamani. 2006. Synergy: A New Algorithm for Property Checking. In Proc. of the ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE'06) (Graz, Austria)."},{"key":"e_1_3_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/CGO.2011.5764696"},{"key":"e_1_3_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/379605.379665"},{"key":"e_1_3_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3338906.3338936"},{"key":"e_1_3_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/800027.808444"},{"key":"e_1_3_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.5555\/2337223.2337308"},{"key":"e_1_3_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491411.2491438"},{"key":"e_1_3_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1044834.1044835"},{"key":"e_1_3_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10515-013-0122-2"},{"key":"e_1_3_2_2_39_1","volume-title":"Proceedings of the Ninth Annual Conference on Object-oriented Programming Systems, Language, and Applications","author":"Plevyak John","unstructured":"John Plevyak and Andrew A. Chien . 1994. Precise Concrete Type Inference for Object-oriented Languages . In Proceedings of the Ninth Annual Conference on Object-oriented Programming Systems, Language, and Applications ( Portland, Oregon, USA) ( OOPSLA'94). John Plevyak and Andrew A. Chien. 1994. Precise Concrete Type Inference for Object-oriented Languages. In Proceedings of the Ninth Annual Conference on Object-oriented Programming Systems, Language, and Applications (Portland, Oregon, USA) ( OOPSLA'94)."},{"key":"e_1_3_2_2_40_1","volume-title":"Dimensions of Precision in Reference Analysis of ObjectOriented Programming Languages. In In Proc. of the 12th International Conference on Compiler Construction (CC'03)","author":"Ryder Barbara G.","year":"2003","unstructured":"Barbara G. Ryder . 2003 . Dimensions of Precision in Reference Analysis of ObjectOriented Programming Languages. In In Proc. of the 12th International Conference on Compiler Construction (CC'03) . Barbara G. Ryder. 2003. Dimensions of Precision in Reference Analysis of ObjectOriented Programming Languages. In In Proc. of the 12th International Conference on Compiler Construction (CC'03)."},{"key":"e_1_3_2_2_41_1","first-page":"189","article-title":"Two approaches to interprocedural data flow analysis. Prentice-Hall, Englewood Clifs, NJ","volume":"7","author":"Sharir Micha","year":"1981","unstructured":"Micha Sharir and Amir Pnueli . 1981 . Two approaches to interprocedural data flow analysis. Prentice-Hall, Englewood Clifs, NJ , Chapter 7 , 189 - 234 . Micha Sharir and Amir Pnueli. 1981. Two approaches to interprocedural data flow analysis. Prentice-Hall, Englewood Clifs, NJ, Chapter 7, 189-234.","journal-title":"Chapter"},{"key":"e_1_3_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_50"},{"key":"e_1_3_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1561\/2500000014"},{"key":"e_1_3_2_2_44_1","volume-title":"Alias Analysis for Object-Oriented Programs","author":"Sridharan Manu","unstructured":"Manu Sridharan , Satish Chandra , Julian Dolby , Stephen J. Fink , and Eran Yahav . 2013. Alias Analysis for Object-Oriented Programs . Springer Berlin Heidelberg , Berlin, Heidelberg , 196-232. Manu Sridharan, Satish Chandra, Julian Dolby, Stephen J. Fink, and Eran Yahav. 2013. Alias Analysis for Object-Oriented Programs. Springer Berlin Heidelberg, Berlin, Heidelberg, 196-232."},{"key":"e_1_3_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2950290.2950296"},{"key":"e_1_3_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/2892208.2892235"},{"key":"e_1_3_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3180155.3180251"},{"key":"e_1_3_2_2_48_1","volume-title":"Proc. of the International Symposium on Software Testing and Analysis (ISSTA'20)","author":"Trabish David","year":"2020","unstructured":"David Trabish and Noam Rinetzky . 2020 . Relocatable Addressing Model for Symbolic Execution . In Proc. of the International Symposium on Software Testing and Analysis (ISSTA'20) (Online). David Trabish and Noam Rinetzky. 2020. Relocatable Addressing Model for Symbolic Execution. In Proc. of the International Symposium on Software Testing and Analysis (ISSTA'20) (Online)."},{"key":"e_1_3_2_2_49_1","volume-title":"Proc. of the Conference on Programing Language Design and Implementation (PLDI'95)","author":"Robert","unstructured":"Robert P. Wilson and Monica S. Lam. 1995. Eficient Context-sensitive Pointer Analysis for C Programs . In Proc. of the Conference on Programing Language Design and Implementation (PLDI'95) (La Jolla, CA, USA). Robert P. Wilson and Monica S. Lam. 1995. Eficient Context-sensitive Pointer Analysis for C Programs. In Proc. of the Conference on Programing Language Design and Implementation (PLDI'95) (La Jolla, CA, USA)."},{"key":"e_1_3_2_2_50_1","volume-title":"Proc. of the 42nd International Conference on Software Engineering (ICSE'20)","author":"W\u00fcstholz Valentin","year":"2018","unstructured":"Valentin W\u00fcstholz and Maria Christakis . 2018 . Targeted Greybox Fuzzing with Static Lookahead Analysis . In Proc. of the 42nd International Conference on Software Engineering (ICSE'20) (Online). Valentin W\u00fcstholz and Maria Christakis. 2018. Targeted Greybox Fuzzing with Static Lookahead Analysis. In Proc. of the 42nd International Conference on Software Engineering (ICSE'20) (Online)."},{"key":"e_1_3_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3180155.3180178"},{"key":"e_1_3_2_2_52_1","volume-title":"Proc. of the IEEE Symposium on Security and Privacy (IEEE S&P'06)","author":"Yang Junfeng","year":"2006","unstructured":"Junfeng Yang , Can Sar , Paul Twohey , Cristian Cadar , and Dawson Engler . 2006 . Automatically generating malicious disks using symbolic execution . In Proc. of the IEEE Symposium on Security and Privacy (IEEE S&P'06) (Oakland, CA, USA). Junfeng Yang, Can Sar, Paul Twohey, Cristian Cadar, and Dawson Engler. 2006. Automatically generating malicious disks using symbolic execution. In Proc. of the IEEE Symposium on Security and Privacy (IEEE S&P'06) (Oakland, CA, USA)."},{"key":"e_1_3_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/1146238.1146255"}],"event":{"name":"ESEC\/FSE '20: 28th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering","location":"Virtual Event USA","acronym":"ESEC\/FSE '20","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering"]},"container-title":["Proceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3368089.3409698","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3368089.3409698","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:44:40Z","timestamp":1750203880000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3368089.3409698"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,11,8]]},"references-count":51,"alternative-id":["10.1145\/3368089.3409698","10.1145\/3368089"],"URL":"https:\/\/doi.org\/10.1145\/3368089.3409698","relation":{},"subject":[],"published":{"date-parts":[[2020,11,8]]},"assertion":[{"value":"2020-11-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}