一句话：提出 Seeker，用 LLM 挖掘惯用模式并实例化为天使式假设来补全缺失代码，以高精度区分开放程序内存安全误报与真实缺陷。
现实中的程序验证常面对“开放程序”，即源码不完整、存在未知代码。传统验证工具对未约束行为采取最坏假设，导致开放程序产生海量虚假告警；而人工构建 mock 模型既耗时又易出错，模型不准还会带来错误的验证结论。本文提出一种能高精度区分潜在内存安全违规中误报与真实缺陷的技术，其核心是对缺失代码做出“天使式假设”。为此，作者先用大语言模型挖掘缓冲区操作程序中的惯用模式，再辅以形式化合成策略，通过属性导向的推理来选取、适配并将这些惯用模式实例化为目标程序上的天使式假设。系统 Seeker 保证：只有当程序能在一组明确定义的“可信”惯用模式下被验证通过时，才判定其正确。在从流行开源软件整理的基准上实验，Seeker 能以零假阴性识别出 79% 的误报。
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. 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.
@article{paperbot2913,
title = {Memory-Safety Verification of Open Programs with Angelic Assumptions},
author = {Gourav Takhar and Baldip Bijlani and Prantik Chatterjee and Akash Lal and Subhajit Roy},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA2},
year = {2025},
doi = {10.1145/3763090}
}