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

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