使用有界模型检验聚焦不动点迭代
Using Bounded Model Checking to Focus Fixpoint Iterations
摘要：
在通过抽象解释的静态分析中，两个经典的不精确性来源是加宽和合并操作。合并操作可以通过区分路径来完成，就像在跟踪分区中一样，代价是枚举指数数量的路径。在这篇文章中，我们描述了如何避免这种系统的探索，集中在一个单一的路径，指定的SMT解决。我们的方法与加速技术结合得很好，因此在某些情况下也可以消除加宽。我们说明了它的公知的凸多面体域。
英文摘要：
Two classical sources of imprecision in static analysis by abstract interpretation are widening and merge operations. Merge operations can be done away by distinguishing paths, as in trace partitioning, at the expense of enumerating an exponential number of paths. In this article, we describe how to avoid such systematic exploration by focusing on a single path at a time, designated by SMT-solving. Our method combines well with acceleration techniques, thus doing away with widenings as well in some cases. We illustrate it over the well-known domain of convex polyhedra.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
