{"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":1776092225394,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":38,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,7,18]],"date-time":"2020-07-18T00:00:00Z","timestamp":1595030400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100003977","name":"Israel Science Foundation","doi-asserted-by":"publisher","award":["1996\/18"],"award-info":[{"award-number":["1996\/18"]}],"id":[{"id":"10.13039\/501100003977","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2020,7,18]]},"DOI":"10.1145\/3395363.3397363","type":"proceedings-article","created":{"date-parts":[[2020,7,13]],"date-time":"2020-07-13T21:44:18Z","timestamp":1594676658000},"page":"51-62","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["Relocatable addressing model for symbolic execution"],"prefix":"10.1145","author":[{"given":"David","family":"Trabish","sequence":"first","affiliation":[{"name":"Tel Aviv University, Israel"}]},{"given":"Noam","family":"Rinetzky","sequence":"additional","affiliation":[{"name":"Tel Aviv University, Israel"}]}],"member":"320","published-online":{"date-parts":[[2020,7,18]]},"reference":[{"key":"e_1_3_2_1_2_1","unstructured":"Rodney M Burstall. 1972. Some techniques for proving correctness of programs which alter data structures. Machine intelligence 7 23-50 ( 1972 ) 3.  Rodney M Burstall. 1972. Some techniques for proving correctness of programs which alter data structures. Machine intelligence 7 23-50 ( 1972 ) 3."},{"key":"e_1_3_2_1_3_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_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1180405.1180445"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1985793.1985995"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2408776.2408795"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1755913.1755932"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1594834.1480921"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/3155562.3155638"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2011.59"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"crossref","unstructured":"Leonardo De Moura and Nikolaj Bj\u00f8rner. 2011. Satisfiability modulo theories: introduction and applications. Commun. ACM 54 9 ( 2011 ) 69-77.  Leonardo De Moura and Nikolaj Bj\u00f8rner. 2011. Satisfiability modulo theories: introduction and applications. Commun. ACM 54 9 ( 2011 ) 69-77.","DOI":"10.1145\/1995376.1995394"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"crossref","unstructured":"Oscar Soria Dustmann Klaus Wehrle and Cristian Cadar. 2018. PARTI: a multiinterval theory solver for symbolic execution.  Oscar Soria Dustmann Klaus Wehrle and Cristian Cadar. 2018. PARTI: a multiinterval theory solver for symbolic execution.","DOI":"10.1145\/3238147.3238179"},{"key":"e_1_3_2_1_14_1","volume-title":"Proc. of the 19th International Conference on Computer-Aided Verification (CAV'07)","author":"Ganesh Vijay","unstructured":"Vijay Ganesh and David L. Dill . 2007. A Decision Procedure for Bit-Vectors and Arrays . In Proc. of the 19th International Conference on Computer-Aided Verification (CAV'07) (Berlin, Germany). Vijay Ganesh and David L. Dill. 2007. A Decision Procedure for Bit-Vectors and Arrays. In Proc. of the 19th International Conference on Computer-Aided Verification (CAV'07) (Berlin, Germany)."},{"key":"e_1_3_2_1_15_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_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_20"},{"key":"e_1_3_2_1_17_1","volume-title":"solc-verify: A modular verifier for Solidity smart contracts. arXiv preprint arXiv","author":"Hajdu \u00c1kos","year":"1907","unstructured":"\u00c1kos Hajdu and Dejan Jovanovi\u0107 . 2019. solc-verify: A modular verifier for Solidity smart contracts. arXiv preprint arXiv : 1907 . 04262 ( 2019 ). \u00c1kos Hajdu and Dejan Jovanovi\u0107. 2019. solc-verify: A modular verifier for Solidity smart contracts. arXiv preprint arXiv: 1907. 04262 ( 2019 )."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/379605.379665"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/2337223.2337279"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3338906.3338936"},{"key":"e_1_3_2_1_21_1","volume-title":"Proc. of the Conference on Programing Language Design and Implementation (PLDI'07)","author":"Lattner Chris","year":"2007","unstructured":"Chris Lattner , Andrew Lenharth , and Vikram Adve . 2007 . Making ContextSensitive Points-to Analysis with Heap Cloning Practical For The Real World . In Proc. of the Conference on Programing Language Design and Implementation (PLDI'07) (San Diego, CA, USA). Chris Lattner, Andrew Lenharth, and Vikram Adve. 2007. Making ContextSensitive Points-to Analysis with Heap Cloning Practical For The Real World. In Proc. of the Conference on Programing Language Design and Implementation (PLDI'07) (San Diego, CA, USA)."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3338906.3338921"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491411.2491438"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2884781.2884807"},{"key":"e_1_3_2_1_25_1","volume-title":"Proc. of the 35th International Conference on Software Engineering (ICSE'13)","author":"Thien Nguyen Hoang Duong","year":"2013","unstructured":"Hoang Duong Thien Nguyen , Dawei Qi , Abhik Roychoudhury , and Satish Chandra . 2013 . SemFix: Program Repair via Semantic Analysis . In Proc. of the 35th International Conference on Software Engineering (ICSE'13) (San Francisco, CA, USA). Hoang Duong Thien Nguyen, Dawei Qi, Abhik Roychoudhury, and Satish Chandra. 2013. SemFix: Program Repair via Semantic Analysis. In Proc. of the 35th International Conference on Software Engineering (ICSE'13) (San Francisco, CA, USA)."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_3"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"crossref","unstructured":"Corina S. P\u0103s\u0103reanu Willem Visser David Bushnell Jaco Geldenhuys Peter Mehlitz and Neha Rungta. 2013. Symbolic PathFinder: integrating symbolic execution with model checking for Java bytecode analysis. (Sept. 2013 ).  Corina S. P\u0103s\u0103reanu Willem Visser David Bushnell Jaco Geldenhuys Peter Mehlitz and Neha Rungta. 2013. Symbolic PathFinder: integrating symbolic execution with model checking for Java bytecode analysis. (Sept. 2013 ).","DOI":"10.1007\/s10515-013-0122-2"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3092703.3092728"},{"key":"e_1_3_2_1_29_1","volume-title":"Proc. of the 24th USENIX Security Symposium (USENIX Security'15)","author":"David","unstructured":"David A. Ramos and Dawson Engler. 2015. Under-constrained Symbolic Execution: Correctness Checking for Real Code . In Proc. of the 24th USENIX Security Symposium (USENIX Security'15) (Washington, D.C., USA). David A. Ramos and Dawson Engler. 2015. Under-constrained Symbolic Execution: Correctness Checking for Real Code. In Proc. of the 24th USENIX Security Symposium (USENIX Security'15) (Washington, D.C., USA)."},{"key":"e_1_3_2_1_30_1","volume-title":"Dimensions of Precision in Reference Analysis of ObjectOriented Programming Languages","author":"Ryder Barbara G.","unstructured":"Barbara G. Ryder . 2003. Dimensions of Precision in Reference Analysis of ObjectOriented Programming Languages . In Compiler Construction, G\u00f6rel Hedin (Ed.). Springer Berlin Heidelberg , Berlin, Heidelberg , 126-137. Barbara G. Ryder. 2003. Dimensions of Precision in Reference Analysis of ObjectOriented Programming Languages. In Compiler Construction, G\u00f6rel Hedin (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 126-137."},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1081706.1081750"},{"key":"e_1_3_2_1_32_1","unstructured":"M. Sharir and A. Pnueli. 1981. Two Approaches to Interprocedural Data Flow Analysis. In Program Flow Analysis: Theory and Applications S.S. Muchnick and N.D. Jones (Eds.). Prentice-Hall Englewood Clifs NJ Chapter 7.  M. Sharir and A. Pnueli. 1981. Two Approaches to Interprocedural Data Flow Analysis. In Program Flow Analysis: Theory and Applications S.S. Muchnick and N.D. Jones (Eds.). Prentice-Hall Englewood Clifs NJ Chapter 7."},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2016.17"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1561\/2500000014"},{"key":"e_1_3_2_1_35_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_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61053-7_58"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"crossref","unstructured":"B. Steensgaard. 1996. Points-to analysis in almost-linear time. In Principles of Programming Languages (POPL).  B. Steensgaard. 1996. Points-to analysis in almost-linear time. In Principles of Programming Languages (POPL).","DOI":"10.1145\/237721.237727"},{"key":"e_1_3_2_1_38_1","volume-title":"Proc. of the ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE'12)","author":"Visser Willem","unstructured":"Willem Visser , Jaco Geldenhuys , and Matthew B. Dwyer . 2012. Green: reducing, reusing and recycling constraints in program analysis . In Proc. of the ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE'12) (Cary, NC, USA). Willem Visser, Jaco Geldenhuys, and Matthew B. Dwyer. 2012. Green: reducing, reusing and recycling constraints in program analysis. In Proc. of the ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE'12) (Cary, NC, USA)."},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/2338965.2336771"}],"event":{"name":"ISSTA '20: 29th ACM SIGSOFT International Symposium on Software Testing and Analysis","location":"Virtual Event USA","acronym":"ISSTA '20","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering"]},"container-title":["Proceedings of the 29th ACM SIGSOFT International Symposium on Software Testing and Analysis"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3395363.3397363","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3395363.3397363","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:38:35Z","timestamp":1750199915000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3395363.3397363"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,7,18]]},"references-count":38,"alternative-id":["10.1145\/3395363.3397363","10.1145\/3395363"],"URL":"https:\/\/doi.org\/10.1145\/3395363.3397363","relation":{},"subject":[],"published":{"date-parts":[[2020,7,18]]},"assertion":[{"value":"2020-07-18","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}