{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,25]],"date-time":"2026-02-25T18:43:03Z","timestamp":1772044983244,"version":"3.50.1"},"reference-count":47,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2021,7,17]],"date-time":"2021-07-17T00:00:00Z","timestamp":1626480000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Archit. Code Optim."],"published-print":{"date-parts":[[2021,12,31]]},"abstract":"<jats:p>Memory safety violations such as buffer overflows are a threat to security to this day. A common solution to ensure memory safety for C is code instrumentation. However, this often causes high execution-time overhead and is therefore rarely used in production.<\/jats:p>\n          <jats:p>Static analyses can reduce this overhead by proving some memory accesses in bounds at compile time. In practice, however, static analyses may fail to verify in-bounds accesses due to over-approximation. Therefore, it is important to additionally optimize the checks that reside in the program.<\/jats:p>\n          <jats:p>\n            In this article, we present PICO, an approach to eliminate\n            <jats:italic>and<\/jats:italic>\n            replace in-bounds checks. PICO exactly captures the spatial memory safety of accesses using Presburger formulas to either verify them statically or substitute existing checks with more efficient ones. Thereby, PICO can generate checks of which each covers multiple accesses and place them at infrequently executed locations.\n          <\/jats:p>\n          <jats:p>We evaluate our LLVM-based PICO prototype with the well-known SoftBound instrumentation on SPEC benchmarks commonly used in related work. PICO reduces the execution-time overhead introduced by SoftBound by 36% on average (and the code-size overhead by 24%). Our evaluation shows that the impact of substituting checks dominates that of removing provably redundant checks.<\/jats:p>","DOI":"10.1145\/3460434","type":"journal-article","created":{"date-parts":[[2021,7,17]],"date-time":"2021-07-17T10:05:22Z","timestamp":1626516322000},"page":"1-27","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["PICO"],"prefix":"10.1145","volume":"18","author":[{"given":"Tina","family":"Jung","sequence":"first","affiliation":[{"name":"Saarland University, SIC, Germany"}]},{"given":"Fabian","family":"Ritter","sequence":"additional","affiliation":[{"name":"Saarland University, SIC, Germany"}]},{"given":"Sebastian","family":"Hack","sequence":"additional","affiliation":[{"name":"Saarland University, SIC, Germany"}]}],"member":"320","published-online":{"date-parts":[[2021,7,17]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"Periklis Akritidis Manuel Costa Miguel Castro and Steven Hand. 2009. Baggy bounds checking: An efficient and backwards-compatible defense against out-of-bounds errors. In SSYM\u201909. 51\u201366. https:\/\/dl.acm.org\/citation.cfm?id=1855772.  Periklis Akritidis Manuel Costa Miguel Castro and Steven Hand. 2009. Baggy bounds checking: An efficient and backwards-compatible defense against out-of-bounds errors. In SSYM\u201909. 51\u201366. https:\/\/dl.acm.org\/citation.cfm?id=1855772."},{"key":"e_1_2_1_2_1","volume-title":"Zima","author":"Bachmann Olaf","year":"1994","unstructured":"Olaf Bachmann , Paul S. Wang , and Eugene V . Zima . 1994 . Chains of recurrences\u2014A method to expedite the evaluation of closed-form functions. In ISSAC\u2019 94. 242\u2013249. Olaf Bachmann, Paul S. Wang, and Eugene V. Zima. 1994. Chains of recurrences\u2014A method to expedite the evaluation of closed-form functions. In ISSAC\u201994. 242\u2013249."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.2307\/1968633"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/349299.349342"},{"key":"e_1_2_1_5_1","volume-title":"CGO\u201911","author":"Bruening Derek","unstructured":"Derek Bruening and Qin Zhao . 2011. Practical memory checking with Dr. Memory . In CGO\u201911 . IEEE Computer Society , 213\u2013223. DOI:https:\/\/doi.org\/10.1109\/CGO.2011.5764689 Derek Bruening and Qin Zhao. 2011. Practical memory checking with Dr. Memory. In CGO\u201911. IEEE Computer Society, 213\u2013223. DOI:https:\/\/doi.org\/10.1109\/CGO.2011.5764689"},{"key":"e_1_2_1_6_1","doi-asserted-by":"crossref","unstructured":"M. G. Burke J.-D. Choi S. Fink D. Grove M. Hind V. Sarkar M. J. Serrano V. C. Sreedhar H. Srinivasan and J. Whaley. 1999. The jalape\u00f1o dynamic optimizing compiler for Java. In JAVA\u2019 99. ACM 129\u2013141. DOI:https:\/\/doi.org\/10.1145\/304065.304113  M. G. Burke J.-D. Choi S. Fink D. Grove M. Hind V. Sarkar M. J. Serrano V. C. Sreedhar H. Srinivasan and J. Whaley. 1999. The jalape\u00f1o dynamic optimizing compiler for Java. In JAVA\u2019 99. ACM 129\u2013141. DOI:https:\/\/doi.org\/10.1145\/304065.304113","DOI":"10.1145\/304065.304113"},{"key":"e_1_2_1_7_1","doi-asserted-by":"crossref","unstructured":"Dinakar Dhurjati and Vikram Adve. 2006. Backwards-compatible array bounds checking for C with very low overhead. In ICSE\u201906. 162\u2013171. DOI:https:\/\/doi.org\/10.1145\/1134285.1134309  Dinakar Dhurjati and Vikram Adve. 2006. Backwards-compatible array bounds checking for C with very low overhead. In ICSE\u201906. 162\u2013171. DOI:https:\/\/doi.org\/10.1145\/1134285.1134309","DOI":"10.1145\/1134285.1134309"},{"key":"e_1_2_1_8_1","volume-title":"Optimal guard synthesis for memory safety","author":"Dillig Thomas","unstructured":"Thomas Dillig , Isil Dillig , and Swarat Chaudhuri . 2014. Optimal guard synthesis for memory safety . In Computer-aided Verification, Armin Biere and Roderick Bloem (Eds.). Springer International Publishing , Cham , 491\u2013507. Thomas Dillig, Isil Dillig, and Swarat Chaudhuri. 2014. Optimal guard synthesis for memory safety. In Computer-aided Verification, Armin Biere and Roderick Bloem (Eds.). Springer International Publishing, Cham, 491\u2013507."},{"key":"e_1_2_1_9_1","volume-title":"CGO\u201917","author":"Doerfert Johannes","unstructured":"Johannes Doerfert , Tobias Grosser , and Sebastian Hack . 2017. Optimistic loop optimization . In CGO\u201917 . IEEE , 292\u2013304. DOI:https:\/\/doi.org\/10.1109\/CGO.2017.7863748 Johannes Doerfert, Tobias Grosser, and Sebastian Hack. 2017. Optimistic loop optimization. In CGO\u201917. IEEE, 292\u2013304. DOI:https:\/\/doi.org\/10.1109\/CGO.2017.7863748"},{"key":"e_1_2_1_10_1","volume-title":"Yap","author":"Duck Gregory J.","year":"2016","unstructured":"Gregory J. Duck and Roland H. C . Yap . 2016 . Heap bounds protection with low fat pointers. In CC\u2019 16. 132\u2013142. DOI:https:\/\/doi.org\/10.1145\/2892208.2892212 Gregory J. Duck and Roland H. C. Yap. 2016. Heap bounds protection with low fat pointers. In CC\u201916. 132\u2013142. DOI:https:\/\/doi.org\/10.1145\/2892208.2892212"},{"key":"e_1_2_1_11_1","volume-title":"CASES\u201909","author":"Ebner Dietmar","unstructured":"Dietmar Ebner , Bernhard Scholz , and Andreas Krall . 2009. Progressive spill code placement . In CASES\u201909 . ACM , New York, NY , 77\u201386. DOI:https:\/\/doi.org\/10.1145\/1629395.1629408 Dietmar Ebner, Bernhard Scholz, and Andreas Krall. 2009. Progressive spill code placement. In CASES\u201909. ACM, New York, NY, 77\u201386. DOI:https:\/\/doi.org\/10.1145\/1629395.1629408"},{"key":"e_1_2_1_12_1","volume-title":"CC\u201901","author":"van Engelen Robert","unstructured":"Robert van Engelen . 2001. Efficient symbolic analysis for optimizing compilers . In CC\u201901 . Springer , London, UK , 118\u2013132. http:\/\/dl.acm.org\/citation.cfm?id=647477.727776. Robert van Engelen. 2001. Efficient symbolic analysis for optimizing compilers. In CC\u201901. Springer, London, UK, 118\u2013132. http:\/\/dl.acm.org\/citation.cfm?id=647477.727776."},{"key":"e_1_2_1_13_1","volume-title":"FoVeOOS\u201910","author":"F\u00e4hndrich Manuel","year":"1807","unstructured":"Manuel F\u00e4hndrich and Francesco Logozzo . 2010. Static contract checking with abstract interpretation . In FoVeOOS\u201910 . Springer , Berlin , 10\u201330. https:\/\/doi.org\/10.1007\/978-3-642- 1807 0-5_2 Manuel F\u00e4hndrich and Francesco Logozzo. 2010. Static contract checking with abstract interpretation. In FoVeOOS\u201910. Springer, Berlin, 10\u201330. https:\/\/doi.org\/10.1007\/978-3-642-18070-5_2"},{"key":"e_1_2_1_14_1","volume-title":"FST TCS\u201902","author":"Finkel Alain","unstructured":"Alain Finkel and J\u00e9r\u00f4me Leroux . 2002. How to compose Presburger-accelerations: Applications to broadcast protocols . In FST TCS\u201902 . Springer , Berlin , 145\u2013156. DOI:https:\/\/doi.org\/10.1007\/3-540-36206-1_14 Alain Finkel and J\u00e9r\u00f4me Leroux. 2002. How to compose Presburger-accelerations: Applications to broadcast protocols. In FST TCS\u201902. Springer, Berlin, 145\u2013156. DOI:https:\/\/doi.org\/10.1007\/3-540-36206-1_14"},{"key":"e_1_2_1_15_1","volume-title":"Rabin","author":"Fischer Michael J.","year":"1998","unstructured":"Michael J. Fischer and Michael O . Rabin . 1998 . Super-exponential complexity of presburger arithmetic. In Quantifier Elimination and Cylindrical Algebraic Decomposition. Springer , 122\u2013135. DOI:https:\/\/doi.org\/10.1007\/978-3-7091-9459-1_5 Michael J. Fischer and Michael O. Rabin. 1998. Super-exponential complexity of presburger arithmetic. In Quantifier Elimination and Cylindrical Algebraic Decomposition. Springer, 122\u2013135. DOI:https:\/\/doi.org\/10.1007\/978-3-7091-9459-1_5"},{"key":"e_1_2_1_16_1","first-page":"27","article-title":"Polly\u2014Performing polyhedral optimizations on a low-level intermediate representation","volume":"22","author":"Grosser Tobias","year":"2012","unstructured":"Tobias Grosser , Armin Gr\u00f6\u00dflinger , and Christian Lengauer . 2012 . Polly\u2014Performing polyhedral optimizations on a low-level intermediate representation . Parallel Proc. Lett. 22 , 4 (2012), 27 . DOI:https:\/\/doi.org\/10.1142\/S0129626412500107 Tobias Grosser, Armin Gr\u00f6\u00dflinger, and Christian Lengauer. 2012. Polly\u2014Performing polyhedral optimizations on a low-level intermediate representation. Parallel Proc. Lett. 22, 4 (2012), 27. DOI:https:\/\/doi.org\/10.1142\/S0129626412500107","journal-title":"Parallel Proc. Lett."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2743016"},{"key":"e_1_2_1_18_1","volume-title":"Cyclone: A type-safe dialect of C. C\/C++ Users J. 23, 1","author":"Grossman Dan","year":"2005","unstructured":"Dan Grossman , Michael Hicks , Trevor Jim , Greg Morrisett , James Cheney , and Yanling Wang . 2005 . Cyclone: A type-safe dialect of C. C\/C++ Users J. 23, 1 (2005), 112\u2013139. Dan Grossman, Michael Hicks, Trevor Jim, Greg Morrisett, James Cheney, and Yanling Wang. 2005. Cyclone: A type-safe dialect of C. C\/C++ Users J. 23, 1 (2005), 112\u2013139."},{"key":"e_1_2_1_19_1","volume-title":"SPEC CPU2006 benchmark descriptions. ACM SIGARCH Comput. Archit. News 34","author":"Henning John L.","year":"2006","unstructured":"John L. Henning . 2006 . SPEC CPU2006 benchmark descriptions. ACM SIGARCH Comput. Archit. News 34 , 4 (Sept. 2006), 1\u201317. DOI:https:\/\/doi.org\/10.1145\/1186736.1186737 John L. Henning. 2006. SPEC CPU2006 benchmark descriptions. ACM SIGARCH Comput. Archit. News 34, 4 (Sept. 2006), 1\u201317. DOI:https:\/\/doi.org\/10.1145\/1186736.1186737"},{"key":"e_1_2_1_20_1","volume-title":"Kelly","author":"Jones Richard W. M.","year":"1997","unstructured":"Richard W. M. Jones and Paul H. J . Kelly . 1997 . Backwards-compatible bounds checking for arrays and pointers in C programs. In AADEBUG\u2019 97. 13\u201326. Richard W. M. Jones and Paul H. J. Kelly. 1997. Backwards-compatible bounds checking for arrays and pointers in C programs. In AADEBUG\u201997. 13\u201326."},{"key":"e_1_2_1_21_1","volume-title":"A Hybrid Approach for Parametric Memory Dependence Analysis. Bachelor\u2019s Thesis","author":"Jung Tina","unstructured":"Tina Jung . 2015. A Hybrid Approach for Parametric Memory Dependence Analysis. Bachelor\u2019s Thesis . Saarland University . Tina Jung. 2015. A Hybrid Approach for Parametric Memory Dependence Analysis. Bachelor\u2019s Thesis. Saarland University."},{"key":"e_1_2_1_22_1","doi-asserted-by":"crossref","unstructured":"Taddeus Kroes Koen Koning Erik van der Kouwe Herbert Bos and Cristiano Giuffrida. 2018. Delta pointers: Buffer overflow checks without the checks. In EuroSys\u201918. ACM. DOI:https:\/\/doi.org\/10.1145\/3190508.3190553  Taddeus Kroes Koen Koning Erik van der Kouwe Herbert Bos and Cristiano Giuffrida. 2018. Delta pointers: Buffer overflow checks without the checks. In EuroSys\u201918. ACM. DOI:https:\/\/doi.org\/10.1145\/3190508.3190553","DOI":"10.1145\/3190508.3190553"},{"key":"e_1_2_1_23_1","volume-title":"LLVM: A compilation framework for lifelong program analysis & transformation. In CGO\u201904","author":"Lattner Chris","year":"2004","unstructured":"Chris Lattner and Vikram Adve . 2004 . LLVM: A compilation framework for lifelong program analysis & transformation. In CGO\u201904 . IEEE Computer Society , 75\u201388. DOI:https:\/\/doi.org\/10.1109\/CGO.2004.1281665 Chris Lattner and Vikram Adve. 2004. LLVM: A compilation framework for lifelong program analysis & transformation. In CGO\u201904. IEEE Computer Society, 75\u201388. DOI:https:\/\/doi.org\/10.1109\/CGO.2004.1281665"},{"key":"e_1_2_1_24_1","unstructured":"LLVM. 2020. LLVM Block Frequency Analysis. https:\/\/llvm.org\/doxygen\/classllvm_1_1BlockFrequ encyInfoImpl.html#details.  LLVM. 2020. LLVM Block Frequency Analysis. https:\/\/llvm.org\/doxygen\/classllvm_1_1BlockFrequ encyInfoImpl.html#details."},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1363686.1363736"},{"key":"e_1_2_1_26_1","volume-title":"POPL\u201914","author":"Long Fan","unstructured":"Fan Long , Stelios Sidiroglou-Douskos , Deokhwan Kim , and Martin Rinard . 2014. Sound input filter generation for integer overflow errors . In POPL\u201914 . ACM , New York, NY , 439\u2013452. DOI:https:\/\/doi.org\/10.1145\/2535838.2535888 Fan Long, Stelios Sidiroglou-Douskos, Deokhwan Kim, and Martin Rinard. 2014. Sound input filter generation for integer overflow errors. In POPL\u201914. ACM, New York, NY, 439\u2013452. DOI:https:\/\/doi.org\/10.1145\/2535838.2535888"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1976.233837"},{"key":"e_1_2_1_28_1","volume-title":"Top 25 Most Dangerous Software Errors","author":"MITRE Corporation","year":"2019","unstructured":"MITRE Corporation . 2019. Top 25 Most Dangerous Software Errors 2019 , Common Weakness Enumeration CWE. https:\/\/cwe.mitre.org\/top25\/archive\/2019\/2019_cw e_top25.html. MITRE Corporation. 2019. Top 25 Most Dangerous Software Errors 2019, Common Weakness Enumeration CWE. https:\/\/cwe.mitre.org\/top25\/archive\/2019\/2019_cw e_top25.html."},{"key":"e_1_2_1_29_1","unstructured":"Santosh Nagarakatte. 2016. SoftBound + CETS for LLVM-3.9. https:\/\/github.com\/santoshn\/SoftBoundCETS-3.9.  Santosh Nagarakatte. 2016. SoftBound + CETS for LLVM-3.9. https:\/\/github.com\/santoshn\/SoftBoundCETS-3.9."},{"key":"e_1_2_1_30_1","volume-title":"SNAPL\u201915","volume":"32","author":"Nagarakatte Santosh","year":"2015","unstructured":"Santosh Nagarakatte , Milo M. K. Martin , and Steve Zdancewic . 2015 . Everything you want to know about pointer-based checking . In SNAPL\u201915 , Vol. 32 . Dagstuhl, Germany, 190\u2013208. DOI:https:\/\/doi.org\/10.4230\/LIPIcs.SNAPL. 2015.190 Santosh Nagarakatte, Milo M. K. Martin, and Steve Zdancewic. 2015. Everything you want to know about pointer-based checking. In SNAPL\u201915, Vol. 32. Dagstuhl, Germany, 190\u2013208. DOI:https:\/\/doi.org\/10.4230\/LIPIcs.SNAPL.2015.190"},{"key":"e_1_2_1_31_1","doi-asserted-by":"crossref","unstructured":"Santosh Nagarakatte Jianzhou Zhao Milo M. K. Martin and Steve Zdancewic. 2009. SoftBound: Highly compatible and complete spatial memory safety for C. In PLDI\u201909. ACM 245\u2013258. DOI:https:\/\/doi.org\/10.1145\/1542476.1542504  Santosh Nagarakatte Jianzhou Zhao Milo M. K. Martin and Steve Zdancewic. 2009. SoftBound: Highly compatible and complete spatial memory safety for C. In PLDI\u201909. ACM 245\u2013258. DOI:https:\/\/doi.org\/10.1145\/1542476.1542504","DOI":"10.1145\/1542476.1542504"},{"key":"e_1_2_1_32_1","volume-title":"OOPSLA\u201914","author":"Nazar\u00e9 H.","unstructured":"H. Nazar\u00e9 , I. Maffra , W. Santos , L. Barbosa , L. Gonnord , and F. M. Q. Pereira . 2014. Validation of memory accesses through symbolic analyses . In OOPSLA\u201914 . ACM , New York, NY , 791\u2013809. DOI:https:\/\/doi.org\/10.1145\/2660193.2660205 H. Nazar\u00e9, I. Maffra, W. Santos, L. Barbosa, L. Gonnord, and F. M. Q. Pereira. 2014. Validation of memory accesses through symbolic analyses. In OOPSLA\u201914. ACM, New York, NY, 791\u2013809. DOI:https:\/\/doi.org\/10.1145\/2660193.2660205"},{"key":"e_1_2_1_33_1","doi-asserted-by":"crossref","unstructured":"George C. Necula Scott McPeak and Westley Weimer. 2002. CCured: Type-safe retrofitting of legacy code. In POPL\u201902. 128\u2013139. DOI:https:\/\/doi.org\/10.1145\/1065887.1065892  George C. Necula Scott McPeak and Westley Weimer. 2002. CCured: Type-safe retrofitting of legacy code. In POPL\u201902. 128\u2013139. DOI:https:\/\/doi.org\/10.1145\/1065887.1065892","DOI":"10.1145\/565816.503286"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1273442.1250746"},{"key":"e_1_2_1_35_1","volume-title":"HiPEAC\u201905","author":"Pop Sebastian","unstructured":"Sebastian Pop , Albert Cohen , and Georges-Andr\u00e9 Silber . 2005. Induction variable analysis with delayed abstractions . In HiPEAC\u201905 . Springer , Berlin , 218\u2013232. DOI:https:\/\/doi.org\/10.1007\/11587514_15 Sebastian Pop, Albert Cohen, and Georges-Andr\u00e9 Silber. 2005. Induction variable analysis with delayed abstractions. In HiPEAC\u201905. Springer, Berlin, 218\u2013232. DOI:https:\/\/doi.org\/10.1007\/11587514_15"},{"key":"e_1_2_1_36_1","volume-title":"PEPM\u201908","author":"Popeea Corneliu","unstructured":"Corneliu Popeea , Dana N. Xu , and Wei-Ngan Chin . 2008. A practical and precise inference and specializer for array bound checks elimination . In PEPM\u201908 . ACM , New York, NY , 177\u2013187. DOI:https:\/\/doi.org\/10.1145\/1328408.1328434 Corneliu Popeea, Dana N. Xu, and Wei-Ngan Chin. 2008. A practical and precise inference and specializer for array bound checks elimination. In PEPM\u201908. ACM, New York, NY, 177\u2013187. DOI:https:\/\/doi.org\/10.1145\/1328408.1328434"},{"key":"e_1_2_1_37_1","volume-title":"PLDI\u201994","author":"Pugh William","unstructured":"William Pugh . 1994. Counting solutions to Presburger formulas: How and why . In PLDI\u201994 . ACM , New York, NY , 121\u2013134. DOI:https:\/\/doi.org\/10.1145\/178243.178254 William Pugh. 1994. Counting solutions to Presburger formulas: How and why. In PLDI\u201994. ACM, New York, NY, 121\u2013134. DOI:https:\/\/doi.org\/10.1145\/178243.178254"},{"key":"e_1_2_1_38_1","unstructured":"Rust. 2020. Rust language manual. https:\/\/www.rust-lang.org\/.  Rust. 2020. Rust language manual. https:\/\/www.rust-lang.org\/."},{"key":"e_1_2_1_39_1","volume-title":"Lam","author":"Ruwase Olatunji","year":"2004","unstructured":"Olatunji Ruwase and Monica S . Lam . 2004 . A practical dynamic buffer overflow detector. In NDSS\u2019 04. 159\u2013169. DOI:https:\/\/doi.org\/10.1145\/780822.781150 Olatunji Ruwase and Monica S. Lam. 2004. A practical dynamic buffer overflow detector. In NDSS\u201904. 159\u2013169. DOI:https:\/\/doi.org\/10.1145\/780822.781150"},{"key":"e_1_2_1_40_1","doi-asserted-by":"crossref","unstructured":"D. Song J. Lettner P. Rajasekaran Y. Na S. Volckaert P. Larsen and M. Franz. 2019. SoK: Sanitizing for security. In SP\u201919. IEEE 1275\u20131295. DOI:https:\/\/doi.org\/10.1109\/SP.2019.00010  D. Song J. Lettner P. Rajasekaran Y. Na S. Volckaert P. Larsen and M. Franz. 2019. SoK: Sanitizing for security. In SP\u201919. IEEE 1275\u20131295. DOI:https:\/\/doi.org\/10.1109\/SP.2019.00010","DOI":"10.1109\/SP.2019.00010"},{"key":"e_1_2_1_41_1","volume-title":"SPEC CPU 2000 benchmarks. https:\/\/www.spec.org\/cpu2000\/.","author":"Standard Performance Evaluation Corporation SPEC.","year":"2000","unstructured":"Standard Performance Evaluation Corporation SPEC. 2000 . SPEC CPU 2000 benchmarks. https:\/\/www.spec.org\/cpu2000\/. Standard Performance Evaluation Corporation SPEC. 2000. SPEC CPU 2000 benchmarks. https:\/\/www.spec.org\/cpu2000\/."},{"key":"e_1_2_1_42_1","doi-asserted-by":"crossref","unstructured":"Laszlo Szekeres Mathias Payer Tao Wei and Dawn Xiaodong Song. 2013. SoK: Eternal war in memory. In S&P\u201913. 48\u201362. DOI:https:\/\/doi.org\/10.1109\/SP.2013.13  Laszlo Szekeres Mathias Payer Tao Wei and Dawn Xiaodong Song. 2013. SoK: Eternal war in memory. In S&P\u201913. 48\u201362. DOI:https:\/\/doi.org\/10.1109\/SP.2013.13","DOI":"10.1109\/SP.2013.13"},{"key":"e_1_2_1_43_1","volume-title":"Andrew Ruef, and Michael Hicks.","author":"Tarditi David","year":"2018","unstructured":"David Tarditi , Archibald Samuel Elliott , Andrew Ruef, and Michael Hicks. 2018 . Checked C: Making C safe by extension. In SecDev\u201918. IEEE , 53\u201360. DOI:https:\/\/doi.org\/10.1109\/SecDev.2018.00015 David Tarditi, Archibald Samuel Elliott, Andrew Ruef, and Michael Hicks. 2018. Checked C: Making C safe by extension. In SecDev\u201918. IEEE, 53\u201360. DOI:https:\/\/doi.org\/10.1109\/SecDev.2018.00015"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1002\/cpe.2939"},{"key":"e_1_2_1_45_1","volume-title":"ICMS\u201910","author":"Verdoolaege Sven","unstructured":"Sven Verdoolaege . 2010. isl: An integer set library for the polyhedral model . In ICMS\u201910 . Springer , Berlin , 299\u2013302. DOI:https:\/\/doi.org\/10.1007\/978-3-642-15582-6_49 Sven Verdoolaege. 2010. isl: An integer set library for the polyhedral model. In ICMS\u201910. Springer, Berlin, 299\u2013302. DOI:https:\/\/doi.org\/10.1007\/978-3-642-15582-6_49"},{"key":"e_1_2_1_46_1","volume-title":"A fresh look at PRE as a maximum flow problem","author":"Xue Jingling","unstructured":"Jingling Xue and Jens Knoop . 2006. A fresh look at PRE as a maximum flow problem . In Compiler Construction, Alan Mycroft and Andreas Zeller (Eds.). Springer , Berlin , 139\u2013154. DOI:https:\/\/doi.org\/10.1007\/11688839_13 Jingling Xue and Jens Knoop. 2006. A fresh look at PRE as a maximum flow problem. In Compiler Construction, Alan Mycroft and Andreas Zeller (Eds.). Springer, Berlin, 139\u2013154. DOI:https:\/\/doi.org\/10.1007\/11688839_13"},{"key":"e_1_2_1_47_1","volume-title":"WPBOUND: Enforcing spatial memory safety efficiently at runtime with weakest preconditions. In ISSRE\u201914","author":"Ye Ding","year":"2014","unstructured":"Ding Ye , Yu Su , Yulei Sui , and Jingling Xue . 2014 . WPBOUND: Enforcing spatial memory safety efficiently at runtime with weakest preconditions. In ISSRE\u201914 . IEEE , Washington, DC , 88\u201399. DOI:https:\/\/doi.org\/10.1109\/ISSRE.2014.20 Ding Ye, Yu Su, Yulei Sui, and Jingling Xue. 2014. WPBOUND: Enforcing spatial memory safety efficiently at runtime with weakest preconditions. In ISSRE\u201914. IEEE, Washington, DC, 88\u201399. DOI:https:\/\/doi.org\/10.1109\/ISSRE.2014.20"}],"container-title":["ACM Transactions on Architecture and Code Optimization"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3460434","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3460434","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:17:04Z","timestamp":1750191424000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3460434"}},"subtitle":["A Presburger In-bounds Check Optimization for Compiler-based Memory Safety Instrumentations"],"short-title":[],"issued":{"date-parts":[[2021,7,17]]},"references-count":47,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2021,12,31]]}},"alternative-id":["10.1145\/3460434"],"URL":"https:\/\/doi.org\/10.1145\/3460434","relation":{},"ISSN":["1544-3566","1544-3973"],"issn-type":[{"value":"1544-3566","type":"print"},{"value":"1544-3973","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,7,17]]},"assertion":[{"value":"2020-09-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-04-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-07-17","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}