Witnesses record automated program analysis results and make them exchangeable. To validate correctness witnesses through abstract interpretation, we introduce a novel abstract operation unassume. This operator incorporates witness invariants into the abstract program state. Given suitable invariants, the unassume operation can accelerate fixpoint convergence and yield more precise results. We demonstrate the feasibility of this approach by augmenting an abstract interpreter with unassume operators and evaluating the impact of incorporating witnesses on performance and precision. Using manually crafted witnesses, we can confirm verification results for multi-threaded programs with a reduction in effort ranging from 7% to 47% in CPU time. More intriguingly, we discover that using witnesses from model checkers can guide our analyzer to verify program properties that it could not verify on its own.

翻译：见证记录了自动化程序分析结果，使其具有可交换性。为了通过抽象解释验证正确性见证，我们引入了一种新颖的抽象操作——unassume。该操作将见证不变量融入抽象程序状态中。在给定合适的不变量后，unassume操作可加速不动点收敛并得出更精确的结果。我们通过向抽象解释器添加unassume操作符，并评估引入见证对性能与精度的影响，验证了该方法的可行性。使用人工构建的见证，我们能够确认多线程程序的验证结果，且CPU时间成本降低7%至47%。更有趣的是，我们发现使用来自模型检查器的见证可引导我们的分析器验证其原本无法独立验证的程序性质。