基于约束的多面体抽象域的弱接合

基于约束的多面体抽象域的处理能力主要受限于其高代价的(强)接合操作，即两多面体的凸闭包计算。针对基于约束的多面体抽象域提出了一系列低代价的弱接合操作，以作为凸闭包计算的可靠替代候选。为了能够在分析效率和精度之间取得合理权衡，还提出了一种启发式策略，以把强、弱接合动态地、有机地结合起来进行程序分析。实验结果表明，弱接合能够极大地提升基于约束的多面体抽象域的效率、可扩展性和鲁棒性。

Weak Join for the Constraint-Based Polyehdra Abstract Domain

The main tractability problem of the constraint-based polyhedra abstract domain can be derived from the costly (strong) join operation, that is, the convex hull computation. This paper presents a series of cheap weak join operations as a sound substitution for the convex hull operation of the constraint-based polyhedra domain. To achieve a trade-off between efficiency and precision, a heuristic strategy is proposed which dynamically combines both strong join and weak join during program analysis. Experimental results show that the weak join operation can significantly improve the efficiency, scalability and robustness of the constraint-based polyhedra domain.