有效地交织加宽和缩小
Efficiently intertwining widening and narrowing
摘要：
非平凡分析问题需要具有无限上升链和下降链的偏序集。为了计算得到的方程组的合理精确的后不动点，Cousot和Cousot建议通过加宽和缩小的方式加速不动点迭代。然而，严格的相位分离可能会不必要地放弃以后无法恢复的精度，因为过度近似的中间结果必须完全通过系统的方程传播。另外，经典的两阶段方法不适合于具有无穷多个未知量的方程组-在那里必须使用需求驱动求解。构建一个相互交织的方法必须能够回答什么时候应用收缩是安全的，或者什么时候必须应用扩展。总的来说，这是一个难题。然而，如果方程的右边是单调的，我们总是可以在到达方程的后不动点时应用窄化。然而，单调性的假设在加宽的情况下不满足。它也不符合方程系统对应的上下文敏感的过程间的分析，可能结合上下文敏感的本地信息与流不敏感的分析全局的分析。作为补救措施，我们提出了一种新的运营商，结合了一个给定的扩大运营商与一个给定的缩小运营商。我们提出了适应版本的循环赛以及工作表迭代，本地和副作用的求解算法的组合运算符，并证明所得到的求解器总是返回声音的结果，并保证终止单调系统时，只有1000多个未知数（约束变量）遇到。实际的补救措施，提出了在非单调的情况下终止。
英文摘要：
Non-trivial analysis problems require posets with infinite ascending and descending chains. In order to compute reasonably precise post-fixpoints of the resulting systems of equations, Cousot and Cousot have suggested accelerated fixpoint iteration by means of widening and narrowing. The strict separation into phases, however, may unnecessarily give up precision that cannot be recovered later, as over-approximated interim results have to be fully propagated through the equation the system. Additionally, classical two-phased approach is not suitable for equation systems with infinitely many unknowns---where demand driven solving must be used. Construction of an intertwined approach must be able to answer when it is safe to apply narrowing---or when widening must be applied. In general, this is a difficult problem. In case the right-hand sides of equations are monotonic, however, we can always apply narrowing whenever we have reached a post-fixpoint for an equation. The assumption of monotonicity, though, is not met in presence of widening. It is also not met by equation systems corresponding to context-sensitive inter-procedural analysis, possibly combining context-sensitive analysis of local information with flow-insensitive analysis of globals. As a remedy, we present a novel operator that combines a given widening operator with a given narrowing operator. We present adapted versions of round-robin as well as of worklist iteration, local and side-effecting solving algorithms for the combined operator and prove that the resulting solvers always return sound results and are guaranteed to terminate for monotonic systems whenever only finitely many unknowns (constraint variables) are encountered. Practical remedies are proposed for termination in the non-monotonic case.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
