先建立可处理的模型
反例引导的抽象细化，英文Counterexample-Guided Abstraction Refinement，简称CEGAR，是把模型检验、反例分析和抽象改进组织成循环的验证方法，而不是某个特定求解器。Clarke、Grumberg、Jha、Lu与Veith在2000年的会议工作及2003年的扩展论文中系统发展了这一方法，用来缓解符号模型检验中的状态空间爆炸。
常见的安全性质验证从过近似抽象开始：合并某些具体状态，或隐藏暂时不重要的变量，但让所有真实行为仍能在抽象模型中得到表示。这样，若抽象模型已经排除所有违规行为，就能在相应保持性条件下推出具体系统安全；若抽象模型报告错误，则不能立即断定真实系统确有错误。
参考：[1]
反例可能来自信息丢失
抽象反例是一条违反待验证性质的抽象执行轨迹。它可能对应真实运行，也可能只是把原本不相容的具体状态合并后形成的假路径。例如，模型忘记两个变量始终相等的关系，就可能把“一者为零、另一者非零”当作可达情况。这里的假路径源自建模损失，而不是程序实际做了这件事。
因此下一步是回到具体语义，检查是否存在满足初始条件、每步转移关系及反例约束的完整运行。2004年的SAT型方法把这项检查构造成可满足性问题：有满足赋值时得到具体反例，不可满足时确认这条抽象轨迹无法实现。只在若干普通测试中没有重现问题，不足以证明它是伪反例。
参考：[2]
细化必须保留真实行为
发现伪反例后，分析器要找出缺失的信息，再增加谓词、恢复变量或拆分被过度合并的状态。以前面示例而言，记录两变量是否相等，可能足以排除那条假路径。重点是用具体系统支持的条件提高精度，而不是修改待验证性质，或直接删除不喜欢的反例。
合格细化应消除已确认的伪行为，同时维持所需的可靠过近似关系。随后重新验证新模型，结果可能是性质得到证明、出现真实错误，或产生另一条需要检查的抽象反例。更精细的模型通常也更大，所以恢复哪些信息会影响每轮的求解开销，不能一味追求全部细节。
结论与停止条件
CEGAR把精度投入集中在阻碍当前证明的部分，适合与符号表示、SAT及其他验证技术结合。它与抽象解释存在理论联系，但二者不是同义词：抽象解释研究语义近似及可靠性框架，CEGAR强调由反例驱动的迭代流程。
方法名称本身不保证所有程序都能在有限时间和内存内得到答案。对有限系统，满足进展条件的细化可能最终达到足够精度，但仍可能遇到很高成本；面对一般无限状态程序，则不能凭反复细化消除不可判定性的限制。达到资源上限或求解器返回未知，只表示本次未得到结论，不能当作安全证明，也不能当作已确认缺陷。