抽象解释(Abstract Interpretation)是形式化验证方法(Formal Verification)的一种,其余的两种分别为定理证明(Theorem Proving)和模型检验(Model Checking)。主要是利用形式化的方法对计算机硬件与软件进行分析验证。

抽象解释理论产生于Cousot.P和Cousot.R于1977年提出的程序静态分析时构造和逼近(approxiamation)程序不动点语义的理论。他们讨论了基于抽象解释理论的程序变换，程序安全性(safety)验证和活性(liveness)的验证。他们利用抽象解释理论作为一种新的形式化验证方法的框架，将各种不同验证工具的近似理论进行统一。

由于模型检验的方法受到状态空间爆炸的限制，定理证明也由于一阶逻辑半可判定的问题，形式化的验证技术难以广泛使用。抽象解释在处理复杂的计算问题或模型的过程中通过对问题进行近似抽象，取出其中的关键部分进行分析，从而减少问题的复杂程度，再综合其他的形式化方法来解决问题。