Abstract: In a highly computer-dependent society，reliability of software，especially of big real-time safety critical ones，gains far-ranging attention from computer community and the rest of the world.Existing tools for formal program verifying have to deal with complex computation through approximating to some extent.Presented by P.Cousot and R.Cousot，abstract interpretation is a theory for sound approximation between mathematic models，and constructs a unifying formal framework for different approximate methods of different program verification tools.Therefore，abstract interpretation is discussed and applied widely in several program analysis and verification fields，including static analysis，program transform，debugging，program watermarking，and so on.This paper first describes the theory framework of abstracting program’s fixpoint semantics，then introduces its state of the art and future challenges.

摘要： 在高度依赖计算机的现代社会，软件（特别是大型实时安全攸关软件）的可靠性成为计算机界和整个社会都非常关注的问题。现有的形式化软件验证工具都不得不通过近似来处理复杂问题中的计算，P.Cousot和R.Cousot提出的抽象解释作为一种在数学模型间进行可靠近似的理论，为各类自动验证工具中不同的近似方法建立起一个统一的形式化框架。抽象解释理论在程序分析和验证研究领域得到了广泛的关注与应用，其应用范围涵盖了程序静态分析、程序变换、程序调试、程序水印等方面。描述了基于程序不动点语义的抽象解释理论框架，并对其近年来的应用现状进行了较为全面的介绍，最后给出了抽象解释理论中尚存在的一些问题及可能的研究方向。