抽象解释全总域模型  

Universe model of abstract interpretation

作　　者：王蓁蓁[1,2] 倪庆剑[3] 张志政[3] 邢汉承[3] 

机构地区：[1]金陵科技学院信息技术学院,江苏南京211169 [2]江苏省信息分析工程实验室,江苏南京211169 [3]东南大学计算机科学和工程学院,江苏南京210096

出　　处：《中国科学技术大学学报》2014年第7期599-604,共6页JUSTC

基　　金：金陵科技学院科研基金(jit-n-201305);2013年度江苏省高校自然科学研究面上自筹经费项目(13KJD520005)资助

摘　　要：抽象解释自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 .

关 键 词：抽象解释 语义 全总域 完备性 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]