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.