抽象解释全总域模型

摘要

抽象解释自1977年提出后，许多作者做了大量工作，将抽象解释理论应用于程序分析和验证研究等领域。本文为有关抽象解释论述构造了一个统一模型，称为抽象解释的全总域模型，目前现存的有关抽象解释文献所采取的框架都相容于全总域模型，且是等价的。在此基础上，我们还提出有关抽象解释理论需要解决的几个基本问题。模型和问题都可以作为今后抽象解释理论发展的参考基点。%Since its introduction in 1977 ,abstract interpretation has inspired a lot of research and is now widely applied in program analyses and verification fields .Therefore ,a universe model was constructed for existing studies on abstract interpretation ,which unifies and is equivalent to all the current frameworks of abstract interpretation . Based on this , several fundamental problems were raised about abstract interpretation that need to be solved .This model and the relevant problems can be viewed as the basic points for further development of abstract interpretation theory .