Static analyses overwhelmingly trade precision for soundness and automation. For this reason, their use-cases are restricted to situations where imprecision isn't prohibitive. In this paper, we propose and specify a static analysis that accepts user-supplied program assumptions that are local to program locations. Such assumptions can be used to counteract imprecision in static analyses, enabling their use in a much wider variety of applications. These assumptions are taken by the analyzer non-deterministically, resulting in a function from sets of accepted assumptions to the resulting analysis under those assumptions. We also demonstrate the utility of such a function in two ways, both of which showcase how it can enable optimization over a search space of assumptions that is otherwise infeasible without the specified analysis.

翻译：静态分析普遍以牺牲精度为代价来确保完备性与自动化。因此，其应用场景通常局限于精度要求不高的场合。本文提出并规范了一种静态分析方法，该方法允许用户提供针对程序位置的局部假设。此类假设可用于抵消静态分析中的不精确性，从而显著拓展其应用范围。分析器以非确定性方式采纳这些假设，生成一个从所采纳假设集合到对应分析结果的映射函数。我们通过两种方式展示了该函数的实用性，均体现了其如何实现对假设搜索空间的优化——这种优化在未采用本方法时通常是难以实现的。