在程序分析与验证中，当问题空间比较复杂难以处理时，用抽象技术去简化问题空间，或者去除待分析对象与问题不相关的细节是一种常用的技术。举例而言，当需要分析的系统在对整型变量x做重复++操作，如果我们从系统可能状态，x的取值，去分析系统状态空间，这会是一个无穷状态系统。而如果把x取值用奇数，偶数两个谓词来抽象，该系统的状态空间立刻可以表达成在奇数和偶数两个状态间切换的系统。也可以用x取值为正数、负数或0三个谓词来抽象，则系统行为可以表达为x从负数跳转到0再跳转到正数这一简单过程。显然，上述两个抽象后得到的系统均远比原无穷状态系统更容易描述与分析。

以上采用的技术被称为谓词抽象（predicate abstraction）。该方法把程序抽象为基于一组有限数量谓词表示的有限状态模型，从而可以使用经典分析或验证算法对其处理。然而抽象模型上得到的结果在真实系统之上并不一定成立。比如，在抽象后的系统中增加了原系统没有的行为，称为过近似（over approximation）。这时抽象后的系统中发现问题并不能代表原系统有问题，因为有可能是抽象过程添加的新行为有问题。而对应的，还有一种抽象被称为下近似（under approximation）。此抽象去掉了原系统中的一些行为从而得到一个简易系统。这时如果分析发现抽象后系统是正确的，事实上可能原系统存在不正确行为，只不过此行为在抽象过程中被去除了而已。

研究人员在如何应对上述问题上投入了大量精力。反例制导的抽象精化方法（counter-example guided abstraction refinement; CEGAR）是其中最重要的技术之一。其基本思路为当抽象后模型违反给定性质时，将相关反例在原系统上进行确认，如确认成立则发现反例，否则分析出抽象过程中导致此虚假反例出现的因素从而对上次抽象进行精化。此方法可以既利用抽象技术带来的优势又不增加误报的可能，因此快速成为软件系统常规模型检验的主要方法，受到广大研究者的青睐，并被应用到多个实际验证工具当中，如SLAM、BLAST等。