开云足球俱乐部-开云综合app登录

国家自然科学基金(611170071),金陵科学学院科研基金(jit-n-201305)\r\n"],"article":{"juan":"51","zhaiyao_cn":"抽象解释由CousotP和CousotR于1977年提出，随后许多作者做了大量工作。本文从不同的角度构造了基于部分等价关系和逻辑部分等价关系一个模型，它与传统抽象解释模型根本不同，该模型并不是对具体系统在“近似”意义上的抽象，而是对原系统上的一切关系（包括逻辑关系）的抽象，因此它不是原系统的“简化”，而是原系统的一个“深化”。从而在此模型上提出的问题具有另外的特征，例如我们提出了复杂性和多态性等问题。","endNoteUrl_en":"https://jns.nju.edu.cn/EN/article/getTxtFile.do?fileType=EndNote&id=526","reference":"[1] CousotP,CousotR. Abstract interpretation: A unified lattice model for static analysis of programs by construction of approximation of fixpoints. In:Proceedingsof the 4thAnnual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Los Angeles, California:ACM Press, 1977, 238~252.
[2] MitchellJC.程序设计语言理论基础. 许满武, 徐建，衷宜. 北京：电子工业出版社，2006,224~460
[3] He H, Gupta N. Automated debugging using path-based weakest preconditions. In: Michel W, Tiziana M. FASE, Lecture Notes in Computer Science: Springer –Verlag, 2004, 2984: 267~280.
[4] CousotP, CousotR.bstract interpretation frameworks.Journal of Logic and Computation, 1992, 2(4):511~547.
[5] CousotP,CousotR. Temporal abstract interpretation. In:Proceedings of the27thACM SIGACT-SIGMOD-SIGART Symposium on Principles of Programming Languages, Boston, MA, USA: ACM Press, 2000, 12~25.
[6] GiacobazziR,RanzatoF,ScozzariF. Making abstract interpretations complete. Journal of the ACM,2000, 47(2): 361~416.
[7] CousotP,CousotR. Systematic design of program analysis frameworks. In:Proceedings of the 6thACM Symposium on Principles of Programming Languages, San Antonio, TX:ACM Press, 1979, 269~282.
[8] RanzatoF,TapparoF. Generalized strong preservation by abstract interpretation.Journal of Logic and Computation, 2007, 17(1): 157~197.
[9] RanzatoF,TapparoF. Strong preservation of temporal fixpoint-based operators by abstract interpretation. In: Proceedings of the 7th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI). LNCS 3855. Charleston, SC, USA: Springer Verlag, 2006, 332~347.
[10] MayerW,StumptnerM. Abstract interpretation of programs for model-based debugging. In: Proceedings of the 20th International Joint Conference on Artificial Intelligence (IJCAI’07), San Francisco, CA, USA: Morgan Kaufmann Publishers Inc, 2007, 471~476.
[11] 王蓁蓁. 模型检验综述. 计算机科学, 2013, 40(6A): 1~14
[12] 高鹰, 陈意云. 基于抽象解释的代码迷惑有效性比较框架. 计算机学报, 2007, 30(5): 806~814.
[13] 杨波, 张明义, 谢刚. 抽象解释理论框架及其应用. 计算机工程与应用, 2010, 46(8): 16~20.
[14] 王蓁蓁, 邢汉承. 逻辑马尔可夫决策过程的正则条件概率理论. 南京大学学报(自然科学), 2013, 49(4): 439~447.
[15] 李梦君, 李舟军, 陈火旺. 抽象解释理论的程序验证技术. 软件学报, 2008, 19(1): 17~26.
[16] 钱俊彦, 赵岭忠, 蔡国永. 基于完备抽象解释的性质强保留抽象研究. 计算机学报, 2014, 37(8): 1754~1766
","bibtexUrl_cn":"//www.sanmikaiseki.com/jns/CN/article/getTxtFile.do?fileType=BibTeX&id=526","abstractUrl_en":"https://jns.nju.edu.cn/EN/Y2015/V51/I2/453","qi":"2","id":526,"nian":2015,"bianHao":"201409053","zuoZheEn_L":"Wang Zhen-zhen1,2*","juanUrl_en":"https://jns.nju.edu.cn/EN/Y2015","shouCiFaBuRiQi":"2015-03-06","qiShiYe":"453","qiUrl_cn":"//www.sanmikaiseki.com/jns/CN/Y2015/V51/I2","lanMu_cn":"","pdfSize":"788097","zuoZhe_CN":"王蓁蓁1,2*","risUrl_cn":"//www.sanmikaiseki.com/jns/CN/article/getTxtFile.do?fileType=Ris&id=526","title_cn":"抽象解释的部分等价逻辑关系模型","jieShuYe":"457","endNoteUrl_cn":"//www.sanmikaiseki.com/jns/CN/article/getTxtFile.do?fileType=EndNote&id=526","zhaiyao_en":"Abstract interpretation was presented by CousotP and CousotR in 1977. Subsequently many scholars have done a lot of studies on it. Generally speaking, the classic abstract interpretation theory is developing within two equivalent formal frameworks of Galois connections and closure operators. This paper constructs a model based on partial equivalence relations and logical partial equivalence relations from a different perspective. It considers the abstract domain as a collection of “partial equivalence relations” and the semantic operator as a collection of “logical partial equivalence relations”. So this model is totally different from the traditional abstract interpretation models. Except that it requires that the concrete or abstract semantic operators have certain logical relations, the model never requires some special properties such as the monotonicity, so in this point it is different from the classic model. Besides, it is not an abstraction of a concrete system in an “approximate” sense, but rather an abstraction of all relations (including logical relations) on the original system. Thus this model is not a “simplification” of the original system but rather a “complication” of the original system.In some sense, it disjoins the “quality” unit from the original system, and it may be more complex than the original system. The advantage of this model is that it embodies some logical relations concerned with the system functions, because itdoes not require that concrete or abstract semantic operations have any special properties (e.g. monotonicity). Therefore here the abstraction is not as the classic understanding. The classic way is to treat some approximation of states as an abstraction, and require that both concrete semantic domains and abstract semantic domains have certain special mathematical structure, for example, lattice or cpo, that is the result of treating “approximation” as the basic essence of abstraction. Whereas our model help structure a concrete system from the semantic domain and the semantic operation the two parts by using partial equivalence relations and logical partial equivalence relations, i.e., it extracts their components separately and finally forms the collection of equivalence classes to discuss the semantic domain and semantic operators. Also, based on such a model, we can discuss the issues that are different from the traditional models, such as the complexity problem and the polymorphism problems, so that it may deepen our understanding for the abstract interpretation theory","bibtexUrl_en":"https://jns.nju.edu.cn/EN/article/getTxtFile.do?fileType=BibTeX&id=526","abstractUrl_cn":"https://jns.nju.edu.cn/CN/Y2015/V51/I2/453","zuoZheCn_L":"王蓁蓁1,2*","juanUrl_cn":"https://jns.nju.edu.cn/CN/Y2015","lanMu_en":"","qiUrl_en":"https://jns.nju.edu.cn/EN/Y2015/V51/I2","zuoZhe_EN":"Wang Zhen-zhen1,2*","risUrl_en":"https://jns.nju.edu.cn/EN/article/getTxtFile.do?fileType=Ris&id=526","title_en":"A logical partial equivalencerelation model of abstract interpretation","hasPdf":"true"},"authorNotes_cn":["(1. 金陵科技学院软件工程学院,南京,211169; 2. 江苏省信息分析工程实验室,南京,211169)"]}">

抽象解释的部分等价逻辑关系模型

王蓁蓁1,2*

南京大学学报(自然科学版)››2015, Vol. 51››Issue (2): 453-457.

PDF(788097 KB)

PDF(788097 KB)

南京大学学报(自然科学版) ›› 2015, Vol. 51 ›› Issue (2) : 453-457.

抽象解释的部分等价逻辑关系模型

{{article.zuoZhe_CN}}

作者信息 +

A logical partial equivalencerelation model of abstract interpretation

{{article.zuoZhe_EN}}

Author information +

文章历史 +

本文亮点

{{article.keyPoints_cn}}

HeighLight

{{article.keyPoints_en}}

摘要

{{article.zhaiyao_cn}}

Abstract

{{article.zhaiyao_en}}

关键词

Key words

本文二维码

引用本文

导出引用

{{article.zuoZheCn_L}}.{{article.title_cn}}[J]. {{journal.qiKanMingCheng_CN}}, 2015, 51(2): 453-457

{{article.zuoZheEn_L}}.{{article.title_en}}[J]. {{journal.qiKanMingCheng_EN}}, 2015, 51(2): 453-457

中图分类号：

参考文献

列表(原文顺序|文献年度倒序|文中引用次数倒序) 可视化分析

参考文献

{{article.reference}}

基金

编委：

主编：

责任编辑：

编辑:

版权

{{article.copyrightStatement_cn}}

{{article.copyrightLicense_cn}}

PDF(788097 KB)

Accesses

Citation

Detail

段落导航

相关文章

/

〈

〉