{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:13:13Z","timestamp":1750219993930,"version":"3.41.0"},"reference-count":28,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2022,9,8]],"date-time":"2022-09-08T00:00:00Z","timestamp":1662595200000},"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":["ACM Trans. Softw. Eng. Methodol."],"published-print":{"date-parts":[[2022,10,31]]},"abstract":"<jats:p>\n            Most\n            <jats:monospace>C<\/jats:monospace>\n            and\n            <jats:monospace>C++<\/jats:monospace>\n            programs use dynamically allocated memory (often known as a heap) to store and organize their data. In practice, it can be useful to compare addresses of different heap objects, for instance, to store them in a binary search tree or a sorted array. However, comparisons of pointers to distinct objects are\u00a0inherently ambiguous: The address order of two objects can be reversed in different executions of the same program, due to the nature of the allocation algorithm and other external factors.\n          <\/jats:p>\n          <jats:p>This poses a significant challenge to program verification, since a sound verifier must consider all possible behaviors of a program, including an arbitrary reordering of the heap. A naive verification of all possibilities, of course, leads to a\u00a0combinatorial explosion of the state space: For this reason, we propose an under-approximating abstract domain that can be soundly refined to consider all relevant heap orderings.<\/jats:p>\n          <jats:p>\n            We have implemented the proposed abstract domain and evaluated it against several existing software verification tools on a\u00a0collection of pointer-manipulating programs. In many cases, existing tools only consider a single fixed heap order, which is a source of unsoundness. We\u00a0demonstrate that using our abstract domain, this unsoundness can be repaired at only a very modest performance cost. Additionally, we show that, even though many verifiers ignore it, ambiguous behavior is present in a considerable fraction of programs from software verification competition (\n            <jats:sc>sv-comp<\/jats:sc>\n            ).\n          <\/jats:p>","DOI":"10.1145\/3508363","type":"journal-article","created":{"date-parts":[[2022,6,27]],"date-time":"2022-06-27T12:52:28Z","timestamp":1656334348000},"page":"1-27","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Verification of Programs Sensitive to\u00a0Heap\u00a0Layout"],"prefix":"10.1145","volume":"31","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5422-5884","authenticated-orcid":false,"given":"Henrich","family":"Lauko","sequence":"first","affiliation":[{"name":"Masaryk University, Czech Republic, Brno, Czech Republic"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1468-1594","authenticated-orcid":false,"given":"Luk\u00e1\u0161","family":"Koren\u010dik","sequence":"additional","affiliation":[{"name":"Masaryk University, Czech Republic, Brno, Czech Republic"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8484-1063","authenticated-orcid":false,"given":"Petr","family":"Ro\u010dkai","sequence":"additional","affiliation":[{"name":"Masaryk University, Czech Republic, Brno, Czech Republic"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2022,9,8]]},"reference":[{"key":"e_1_3_2_2_2","unstructured":"2020. Do not subtract or compare two pointers \u2013 SEI CERT C Coding Standard \u2013 Confluence. Retrieved from https:\/\/wiki.sei.cmu.edu\/confluence\/display\/c\/ARR36-C.+Do+not+subtract+or+compare+two+pointers+that+do+not+refer+to+the+same+array."},{"key":"e_1_3_2_3_2","first-page":"7","article-title":"Analysis tool evaluation: Coverity prevent","author":"Almossawi Ali","year":"2006","unstructured":"Ali Almossawi, Kelvin Lim, and Tanmay Sinha. 2006. Analysis tool evaluation: Coverity prevent. Carnegie Mellon University, Pittsburgh, PA., 7\u201311. https:\/\/www.cs.cmu.edu\/aldrich\/courses\/654-sp07\/tools\/cure-coverity-06.pdf.","journal-title":"Carnegie Mellon University, Pittsburgh, PA."},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1145\/3182657"},{"key":"e_1_3_2_5_2","volume-title":"Automated Technology for Verification and Analysis","author":"Baranov\u00e1 Zuzana","year":"2017","unstructured":"Zuzana Baranov\u00e1, Ji\u0159\u00ed Barnat, Katar\u00edna Kejstov\u00e1, Tade\u00e1\u0161 Ku\u010dera, Henrich Lauko, Jan Mr\u00e1zek, Petr Ro\u010dkai, and Vladim\u00edr \u0160till. 2017. Model checking of C and C++ with DIVINE 4. In Automated Technology for Verification and Analysis. Springer International Publishing, Cham."},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_16"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(96)00191-0"},{"key":"e_1_3_2_8_2","first-page":"209","volume-title":"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 8th USENIX Conference on Operating Systems Design and Implementation (OSDI\u201908). USENIX Association, 209\u2013224."},{"key":"e_1_3_2_9_2","first-page":"380","volume-title":"IEEE Symposium on Security and Privacy (SP\u201912)","author":"Cha Sang Kil","year":"2012","unstructured":"Sang Kil Cha, Thanassis Avgerinos, Alexandre Rebert, and David Brumley. 2012. Unleashing mayhem on binary code. In IEEE Symposium on Security and Privacy (SP\u201912). IEEE Computer Society, 380\u2013394."},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-45237-7"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_15"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"e_1_3_2_13_2","first-page":"21","volume-title":"European Symposium on Programming","author":"Cousot Patrick","year":"2005","unstructured":"Patrick Cousot, Radhia Cousot, J\u00e9r\u00f4me Feret, Laurent Mauborgne, Antoine Min\u00e9, David Monniaux, and Xavier Rival. 2005. The ASTR\u00c9E analyzer. In European Symposium on Programming. Springer, 21\u201330."},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_29"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/1064978.1065036"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_2"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00268497"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.5555\/1765871.1765924"},{"key":"e_1_3_2_19_2","volume-title":"24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software","author":"Kokologiannakis Michalis","year":"2017","unstructured":"Michalis Kokologiannakis and Konstantinos Sagonas. 2017. Stateless model checking of the Linux kernel\u2019s hierarchical read-copy-update (tree RCU). In 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software."},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_26"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-02508-3_17"},{"key":"e_1_3_2_22_2","first-page":"1","article-title":"Template-based verification of heap-manipulating programs","author":"Mal\u00edk Viktor","year":"2018","unstructured":"Viktor Mal\u00edk, Martin Hruska, P. Schrammel, and T. Vojnar. 2018. Template-based verification of heap-manipulating programs. In Formal Methods in Computer Aided Design Conference (FMCAD\u201918). 1\u20139.","journal-title":"Formal Methods in Computer Aided Design Conference (FMCAD\u201918)"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-006-8609-1"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_31"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2018.04.026"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49674-9_56"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1145\/1095430.1081750"},{"key":"e_1_3_2_28_2","article-title":"The GCC developer community","author":"Stallman Richard M.","year":"2003","unstructured":"Richard M. Stallman. 2003. The GCC developer community. Using GCC: The GNU Compiler Collection Reference Manual (2003). https:\/\/gcc.gnu.org\/onlinedocs\/gcc-4.6.1\/gcc.pdf.","journal-title":"Using GCC: The GNU Compiler Collection Reference Manual"},{"key":"e_1_3_2_29_2","doi-asserted-by":"crossref","first-page":"385","DOI":"10.1007\/978-3-540-70545-1_36","volume-title":"Computer Aided Verification","author":"Yang Hongseok","year":"2008","unstructured":"Hongseok Yang, Oukseh Lee, Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, and Peter O\u2019Hearn. 2008. Scalable shape analysis for systems code. In Computer Aided Verification, Aarti Gupta and Sharad Malik (Eds.). Springer Berlin, 385\u2013398."}],"container-title":["ACM Transactions on Software Engineering and Methodology"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3508363","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3508363","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T17:49:36Z","timestamp":1750182576000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3508363"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,9,8]]},"references-count":28,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2022,10,31]]}},"alternative-id":["10.1145\/3508363"],"URL":"https:\/\/doi.org\/10.1145\/3508363","relation":{},"ISSN":["1049-331X","1557-7392"],"issn-type":[{"type":"print","value":"1049-331X"},{"type":"electronic","value":"1557-7392"}],"subject":[],"published":{"date-parts":[[2022,9,8]]},"assertion":[{"value":"2021-03-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-12-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2022-09-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}