Correctness kernels of abstract interpretations

被引:3
|
作者
Giacobazzi, Roberto [1 ]
Ranzato, Francesco [2 ]
机构
[1] Univ Verona, I-37100 Verona, Italy
[2] Univ Padua, Dipartimento Matemat, I-35100 Padua, Italy
关键词
STRONG PRESERVATION; REFINEMENT;
D O I
10.1016/j.ic.2014.02.003
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
In abstract interpretation-based static analysis, approximation is encoded by abstract domains. They provide systematic guidelines for designing abstract semantic functions that approximate some concrete system behaviors under analysis. It may happen that an abstract domain contains redundant information for the specific purpose of approximating a given concrete semantic function. This paper introduces the notion of correctness kernel of an abstract interpretation, a methodology for simplifying abstract domains, i.e. removing abstract values from them, in a maximal way while retaining exactly the same approximate behavior of the system under analysis. We show that in abstract model checking correctness kernels provide a simplification paradigm of the abstract state space that is guided by examples, meaning that this simplification preserves spuriousness of examples (i.e., abstract paths). In particular, we show how correctness kernels can be integrated with the well-known CEGAR (CounterExample-Guided Abstraction Refinement) methodology. (C) 2014 Elsevier Inc. All rights reserved.
引用
收藏
页码:187 / 203
页数:17
相关论文
共 50 条
  • [21] Jupiter Made Abstract, and Then Refined
    Heng-Feng Wei
    Rui-Ze Tang
    Yu Huang
    Jian Lv
    Journal of Computer Science and Technology, 2020, 35 : 1343 - 1364
  • [22] Preserving correctness of requirements evolution through refinement in Event-B
    Traichaiyaporn, Kriangkrai
    Aoki, Toshiaki
    2013 20TH ASIA-PACIFIC SOFTWARE ENGINEERING CONFERENCE (APSEC 2013), VOL 1, 2013, : 315 - 322
  • [23] Making abstract models complete
    Giacobazzi, Roberto
    Mastroeni, Isabella
    MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE, 2016, 26 (04) : 658 - 701
  • [24] Refinement of Operator-valued Reproducing Kernels
    Zhang, Haizhang
    Xu, Yuesheng
    Zhang, Qinghui
    JOURNAL OF MACHINE LEARNING RESEARCH, 2012, 13 : 91 - 136
  • [25] Symbolic Abstract Data Type Inference
    Emmi, Michael
    Enea, Constantin
    ACM SIGPLAN NOTICES, 2016, 51 (01) : 513 - 525
  • [26] Abstract State Machines and the Inquiry Process
    Huggins, James K.
    Wallace, Charles
    FIELDS OF LOGIC AND COMPUTATION: ESSAYS DEDICATED TO YURI GUREVICH ON THE OCCASION OF HIS 70TH BIRTHDAY, 2010, 6300 : 405 - +
  • [27] Kernels and cokernels in the category of augmented involutive stereotype algebras
    Akbarov, S. S.
    JOURNAL OF ALGEBRA AND ITS APPLICATIONS, 2020, 19 (06)
  • [28] A SHARPENED VERSION OF ACZEL INEQUALITY BY ABSTRACT CONVEXITY
    Tinaztepe, Ramazan
    Tinaztepe, Gultekin
    MATHEMATICAL INEQUALITIES & APPLICATIONS, 2021, 24 (03): : 635 - 643
  • [29] Probabilistic Modal Specifications (Invited Extended Abstract)
    Larsen, Kim G.
    Legay, Axel
    FORMAL ASPECTS OF COMPONENT SOFTWARE, 2014, 8348 : 1 - 4
  • [30] Automatic Construction of Complete Abstraction by Abstract Interpretation
    Qian, Junyan
    Zhao, Lingzhong
    Cai, Guoyong
    Gu, Tianlong
    PROCEEDINGS OF THE 8TH IEEE/ACIS INTERNATIONAL CONFERENCE ON COMPUTER AND INFORMATION SCIENCE, 2009, : 927 - +