{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,25]],"date-time":"2026-06-25T03:41:02Z","timestamp":1782358862771,"version":"3.54.5"},"reference-count":72,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,10,9]]},"abstract":"<jats:p>An open program is one for which the complete source code is not available, which is a reality for real-world program verification. Software verification tools tend to assume the worst about any unconstrained behavior and this can yield an enormous number of spurious warnings for open programs. For any serious verification effort, the engineer must invest time up-front in building a suitable model (or mock) of any missing code, which is time-consuming and error-prone. Inaccuracies in the mocks can lead to incorrect verification results.<\/jats:p>\n          <jats:p>In this paper, we demonstrate a technique that is capable of distinguishing between false positives and actual bugs from potential memory-safety violations in an open program with high accuracy. Central to the technique is the ability of making angelic assumptions about missing code. To accomplish this, we first mine a set of idiomatic patterns in buffer-manipulating programs using a large language model (LLM). This is complemented by a formal synthesis strategy that performs property-directed reasoning to select, adapt and instantiate these idiomatic patterns into angelic assumptions on the target program. Overall, our system, Seeker, guarantees that a program is deemed correct only if it can be verified under a well-defined set of \"trusted\" idiomatic patterns. In our experiments over a set of benchmarks curated from popular open-source software, our tool Seeker is able to identify 79% of the false positives with zero false negatives.<\/jats:p>","DOI":"10.1145\/3763090","type":"journal-article","created":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T08:51:31Z","timestamp":1759999891000},"page":"1119-1147","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Memory-Safety Verification of Open Programs with Angelic Assumptions"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8700-3428","authenticated-orcid":false,"given":"Gourav","family":"Takhar","sequence":"first","affiliation":[{"name":"Indian Institute of Technology Kanpur, Kanpur, India"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-0436-6413","authenticated-orcid":false,"given":"Baldip","family":"Bijlani","sequence":"additional","affiliation":[{"name":"Indian Institute of Technology Kanpur, Kanpur, India"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3320-9543","authenticated-orcid":false,"given":"Prantik","family":"Chatterjee","sequence":"additional","affiliation":[{"name":"Indian Institute of Technology Kanpur, Kanpur, India"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0002-4359-9378","authenticated-orcid":false,"given":"Akash","family":"Lal","sequence":"additional","affiliation":[{"name":"Microsoft Research, Bengaluru, India"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3394-023X","authenticated-orcid":false,"given":"Subhajit","family":"Roy","sequence":"additional","affiliation":[{"name":"Indian Institute of Technology Kanpur, Kanpur, India"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,10,9]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"[n. d.]. 0day \u201cIn the Wild\". https:\/\/googleprojectzero.blogspot.com\/p\/0day.html Accessed: 2023-01-08"},{"key":"e_1_2_1_2_1","unstructured":"[n. d.]. Trends challenges and strategic shifts in the software vulnerability mitigation landscape. https:\/\/github.com\/microsoft\/MSRC-Security-Research\/blob\/master\/presentations\/2019_02_BlueHatIL\/2019_01%20-%20BlueHatIL%20-%20Trends%2C%20challenge%2C%20and%20shifts%20in%20software%20vulnerability%20mitigation.pdf Accessed: 2023-01-08"},{"key":"e_1_2_1_3_1","unstructured":"[n. d.]. Verisec benchmarks. https:\/\/github.com\/tomhart-msc\/verisec Accessed: 2023-01-08"},{"key":"e_1_2_1_4_1","unstructured":"2023. CVE \u2014 Common Vulnerabilities and Exposures.. https:\/\/cve.mitre.org\/"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","unstructured":"2025. Artifact for Memory-Safety Verification of Open Programs with Angelic Assumptions. https:\/\/doi.org\/10.5281\/zenodo.15760792 10.5281\/zenodo.15760792","DOI":"10.5281\/zenodo.15760792"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837628"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040314"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_52"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-13185-1_3"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676977"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3001854.3001860"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2983990.2984014"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462188"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20398-5_33"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1985793.1985811"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36577-X_24"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1322263.1322283"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_19"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1143844.1143874"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_46"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254087"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-48288-9_7"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/COMPSAC51774.2021.00194"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2019.2943546"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1081706.1081713"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_2_1_28_1","unstructured":"Lei Huang Weijiang Yu Weitao Ma Weihong Zhong Zhangyin Feng Haotian Wang Qianglong Chen Weihua Peng Xiaocheng Feng Bing Qin et al. 2023. A survey on hallucination in large language models: Principles taxonomy challenges and open questions. arXiv preprint arXiv:2311.05232."},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3482909.3482915"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993550"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.34727\/2022\/isbn.978-3-85448-053-2_37"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563334"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-74776-2_6"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3733716"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-023-00420-3"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","unstructured":"Adharsh Kamath Nausheen Mohammed Aditya Senthilnathan Saikat Chakraborty Pantazis Deligiannis Shuvendu K. Lahiri Akash Lal Aseem Rastogi Subhajit Roy and Rahul Sharma. 2024. Leveraging LLMs for Program Verification. In FMCAD. 107\u2013118. https:\/\/doi.org\/10.34727\/2024\/isbn.978-3-85448-065-5_16 10.34727\/2024\/isbn.978-3-85448-065-5_16","DOI":"10.34727\/2024\/isbn.978-3-85448-065-5_16"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44898-5_16"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30482-1_23"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/1321631.1321691"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3691620.3695015"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3533767.3534381"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.34727\/2020\/isbn.978-3-85448-042-6_24"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_32"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/2813885.2738002"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1002\/spe.515"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1109\/SCAM63643.2024.00024"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571208"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE55347.2025.00023"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-65627-9_24"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563332"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","unstructured":"Gary Mullen and Liam Meany. 2019. Assessment of Buffer Overflow Based Attacks On an IoT Operating System. In 2019 Global IoT Summit (GIoTS). 1\u20136. https:\/\/doi.org\/10.1109\/GIOTS.2019.8766434 10.1109\/GIOTS.2019.8766434","DOI":"10.1109\/GIOTS.2019.8766434"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542504"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908099"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/3293882.3330554"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2021.3120349"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454104"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133889"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_7"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40001.2021.00060"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236024.3236084"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/3188720"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1109\/ESEM.2017.57"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/2914770.2837655"},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99524-9_1"},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","unstructured":"Gourav Takhar and Subhajit Roy. 2023. SR-SFLL: Structurally Robust Stripped Functionality Logic Locking. In Computer Aided Verification Constantin Enea and Akash Lal (Eds.). Springer Nature Switzerland Cham. 190\u2013212. https:\/\/doi.org\/10.1007\/978-3-031-37709-9_10 10.1007\/978-3-031-37709-9_10","DOI":"10.1007\/978-3-031-37709-9_10"},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1145\/3617555.3617874"},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/3368826.3377910"},{"key":"e_1_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1145\/3106237.3106263"},{"key":"e_1_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-021-00387-z"},{"key":"e_1_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485493"},{"key":"e_1_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-03542-0_21"},{"key":"e_1_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1145\/1029894.1029911"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3763090","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T17:41:32Z","timestamp":1760031692000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3763090"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,9]]},"references-count":72,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2025,10,9]]}},"alternative-id":["10.1145\/3763090"],"URL":"https:\/\/doi.org\/10.1145\/3763090","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,10,9]]},"assertion":[{"value":"2025-03-25","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-08-12","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-10-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}