Craig插值是用于模型检测中抽象精化的一种高效方法，而不同类型的插值对模型检测器的性能有不同的促进作用：有的使其收敛，有的使其发散。为求得促使模型检测器快速收敛的插值，插值抽象技术应运而生，基于此，插值求解问题被转换为抽象格中抽象边界的搜索问题。本文对已有算法进行了改进，提出了两个新的启发式搜索算法，以促使抽象边界的搜索更加高效和精准。　　J.Leroux和P.Ruemmer所提算法的基本思想是，基于深度优先搜索和二分法，从可行元素出发进行搜索，当找到一个可行元素其满足所有直接后继均不可行时，该元素即为所求抽象边界中的元素。然而，当系统规模扩大时，由于抽象边界中元素的序关系较大，因此搜索路径会变长，遍历的元素会大幅增加，搜索效率则相应降低。针对此问题，本文提出了基于宽度优先搜索的抽象边界搜索算法，该算法从格顶端出发，由上往下逐层搜索，并将所搜索到的可行元素的前趋全部删除，从而对搜索空间进行了大幅削减。此外，本文不仅给出了该算法的正确性和终止性证明，而且从定性和定量角度分析了该算法的效率，并通过具体例子说明了该算法的效率相较于原算法较高。　　为了对抽象边界进行精化，使其中所含元素质量尽可能的好，即能更好地促进模型检测器的更快速收敛，本文在基于宽度优先搜索的抽象边界搜索算法的基础上，引入了具有反单调性的估价函数，提出了估价函数指引的抽象边界的精化搜索算法，并证明了该算法的终止性和正确性，而且通过定性和定量角度对该算法的效率进行了分析，并借助具体实例阐明了该算法的执行过程，说明了该算法不仅使得抽象边界得到了精化，更有效地削减了搜索空间，促进算法效率的提高。