抽象解释全总域模型

doi:10.3969/j.issn.0253-2778.2014.07.009

中国科学技术大学学报 ›› 2014, Vol. 44 ›› Issue (7): 599-604.DOI: 10.3969/j.issn.0253-2778.2014.07.009

抽象解释全总域模型

王蓁蓁，倪庆剑，张志政，邢汉承

1.金陵科技学院信息技术学院，江苏南京 211169; 2.江苏省信息分析工程实验室，江苏南京 211169; 3.东南大学计算机科学和工程学院，江苏南京 210096

收稿日期:2014-03-21 修回日期:2014-06-15 接受日期:2014-06-15 出版日期:2023-05-11 发布日期:2014-06-15
通讯作者: 王蓁蓁
作者简介:王蓁蓁(通讯作者)，女，1975年生，博士后/副教授. 研究方向：软件测试，人工智能，程序分析.
基金资助:
金陵科技学院科研基金（jit-n-201305），2013年度江苏省高校自然科学研究面上自筹经费项目（13KJD520005）资助.

Universe model of abstract interpretation

WANG Zhenzhen, NI Qingjian, ZHANG Zhizheng, XING Hancheng

1.School of Information Technology, Jinling Institute of Technology, Nanjing 211169, China; 2.Information Analysis Engineering Laboratory of Jiangsu Province, Nanjing 211169, China; 3.School of Computer Science & Engineering, Southeast University, Nanjing 210096, China

Received:2014-03-21 Revised:2014-06-15 Accepted:2014-06-15 Online:2023-05-11 Published:2014-06-15

摘要/Abstract

摘要： 抽象解释自1977年提出后，许多作者做了大量工作，将抽象解释理论应用于程序分析和验证研究等领域.本文为有关抽象解释论述构造了一个统一模型，称为抽象解释的全总域模型，目前现存的有关抽象解释文献所采取的框架都相容于全总域模型，且是等价的.在此基础上，我们还提出有关抽象解释理论需要解决的几个基本问题.模型和问题都可以作为今后抽象解释理论发展的参考基点.

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

Abstract: 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.

Key words: abstract interpretation, semantics, universe domain, completeness

中图分类号:

TP31

王蓁蓁，倪庆剑，张志政，邢汉承. 抽象解释全总域模型[J]. 中国科学技术大学学报, 2014, 44(7): 599-604.

WANG Zhenzhen, NI Qingjian, ZHANG Zhizheng, XING Hancheng. Universe model of abstract interpretation[J]. Journal of University of Science and Technology of China, 2014, 44(7): 599-604.

参考文献

［1］ Cousot P, Cousot, R. Temporal abstract interpretation ［C］// Proceedings of the 27th ACM Symposium on Principles of Programming Languages. Boston, USA: ACM Press, 2000: 12-25.
［2］ Giacobazzi R, Ranzato F, Scozzari F. Making abstract interpretations complete ［J］. Journal of the ACM 2000, 47(2): 361-416.
［3］ Cousot P, Cousot R. Systematic design of program analysis frameworks ［C］ // Proceedings of the 6th ACM Symposium on Principles of Programming Languages. San Antonio, USA: ACM Press, 1979: 269-282.
［4］ Cousot P, Cousot R. Abstract interpretation frameworks ［J］. Journal of Logic and Computation, 1992, 2(4): 511-547.
［5］ Mitchell J C.程序设计语言理论基础［M］. 许满武, 徐建, 衷宜, 等译, 北京: 电子工业出版社, 2006.
［6］ Cousot P, Cousot R. Abstract interpretation: A unified lattice model for static analysis of programs by construction of approximation of fixpoints ［C］ // Proceedings of the 6th Annual ACM Symposium on Principles of Programming Languages. Los Angeles, USA: ACM Press, 1977: 238-252.
［7］ Ranzato F, Tapparo F. Generalized strong preservation by abstract interpretation ［J］. Journal of Logic and Computation, 2007, 17(1): 157-197.
［8］ Ranzato F, Tapparo F. Strong preservation of temporal fixpoint-based operators by abstract interpretation ［C］// Proceedings of the 7th International Conference on Verification, Model Checking, and Abstract Interpretation. Charleston, USA: Springer, 2006: 332-347.
［9］ Mayer W, Stumptner M. Abstract interpretation of programs for model-based debugging ［C］// Proceedings of the 20th International Joint Conference on Artificial Intelligence. San Francisco, USA: Morgan Kaufmann Publishers, 2007: 471-476.
［10］高鹰, 陈意云. 基于抽象解释的代码迷惑有效性比较框架［J］. 计算机学报, 2007, 30(5): 806-814.
［11］杨波, 张明义, 谢刚. 抽象解释理论框架及其应用［J］. 计算机工程与应用, 2010, 46(8): 16-20.
［12］李梦君, 李舟军, 陈火旺. 抽象解释理论的程序验证技术［J］. 软件学报, 2008, 19(1): 17-26.

[1]	赵柳，陆军，刘杨. MAEA-DeepLab：具有多特征注意力有效聚合模块的语义分割网络[J]. 中国科学技术大学学报, 2020, 50(8): 1170-1180.
[2]	邱镇，王琪媛，刘迪，孟洪民. 一种基于可伸缩模式的潜在语义挖掘方法[J]. 中国科学技术大学学报, 2019, 49(7): 524-532.
[3]	王根生，潘方正. 融合语义相似度的协同过滤推荐算法[J]. 中国科学技术大学学报, 2019, 49(10): 835-841.
[4]	方建生，许言午，蔡瑞初，秦艳. 一种基于Skill-LFM的知识点推荐方法[J]. 中国科学技术大学学报, 2018, 48(9): 755-761.
[5]	王述，史忠植. 基于深度典型相关性分析的跨媒体语义检索[J]. 中国科学技术大学学报, 2018, 48(4): 322-330.
[6]	王渊，孙樱郡，王博，杨朝洲，杨量. 在线社会关系语义化度量的可视化分析[J]. 中国科学技术大学学报, 2018, 48(4): 314-321.
[7]	蔡圆媛，卢苇. 基于低维语义向量模型的语义相似度度量[J]. 中国科学技术大学学报, 2016, 46(9): 719-726.
[8]	谢兴生，周邦定，熊焰. 一种基于框架语义的专项新闻检索方法研究[J]. 中国科学技术大学学报, 2016, 46(3): 253-258.
[9]	季铎，毕臣，蔡东风. 基于类别信息优化的潜在语义分析分类技术[J]. 中国科学技术大学学报, 2015, 45(4): 314-320.

抽象解释全总域模型

Universe model of abstract interpretation

PDF (PC)

可视化

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 9

编辑推荐

Metrics

本文评价