抽象解释（abstraction interpretation），理学-计算机科学技术-计算机软件-软件基础理论-程序验证，一种用于对计算机科学中复杂数学结构进行抽象和近似的理论。抽象解释理论由法国科学家P.库索[注]（Patrick Cousot，1948-12-03～ ）和R.库索[注]（Radhia Cousot）于20世纪70年代提出。其最初主要以计算机程序的语义为研究对象，提供了一个统一的理论框架来对程序语义进行抽象和推理，并在静态分析领域得到了广泛应用。对复杂系统进行推理往往需要将描述其实际行为的具体语义抽象为更本质、更简单的抽象语义，使得在抽象语义上进行的推理更易于自动化、复杂度更低、效率更高。本质上，抽象解释是通过不同程度的抽象和近似，在推理能力和计算代价之间取得合理权衡。一般而言，设计抽象语义时会考虑原系统所有的实际行为，使得抽象语义描述的行为集合是原系统实际行为集合的超集，可能包含一些原系统中实际不存在的行为。在这种情况下，称抽象语义是具体语义的保守抽象（也称上近似抽象）。