ISSN 0253-2778

CN 34-1054/N

open
Free to Publish. Free to Read.
Open AccessOpen Access JUSTC Original Paper

Universe model of abstract interpretation

  • 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

Cite this:
https://doi.org/10.3969/j.issn.0253-2778.2014.07.009
  • Received Date: 21 March 2014
  • Accepted Date: 15 June 2014
  • Rev Recd Date: 15 June 2014
  • Publish Date: 30 July 2014
    Abstract

  • 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.

    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.
    • FullText(HTML)
  • loading
    • References(12)
  • [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.
    • Supplements(0)
    • Related Articles
    • Track Citations
  • 加载中

Catalog

    |
    Get Citation
    PDF
    XML
    [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.
    Recommended articles
    TrendMD
    Volume 44 Issue 7 page: 599-604
    Cover

    Article Metrics

    Article views (43) PDF downloads(85)
    Proportional views

    Copyright © Editorial Office of JUSTC, All Rights Reserved. 皖ICP备05002528号

    Supported by: Beijing Renhe Information Technology Co. Ltd    

    /

    DownLoad:  Full-Size Img  PowerPoint
    Return
    Return