A Survey on Product Operators in Abstract Interpretation
A Survey on Product Operators in Abstract Interpretation
复制标题
抽象解释中的产品算子调查
DOI：
10.4204/eptcs.129.19
复制
发表时间：
2013
期刊：
影响因子：
5.6
通讯作者：
Pietro Ferrara
中科院分区：
文献类型：
--
作者：
Agostino Cortesi;Giulia Costantini;Pietro Ferrara
解释（6）已经被广泛地应用为用于计算机程序的语义的合理近似的通用技术。特别是，抽象域（表示数据）和语义（表示数据操作）近似于具体计算。当分析一个程序并试图证明它的某些性质时，结果的质量取决于抽象域的选择。在分析的准确性和效率之间总是有一个权衡。多年来，各种抽象领域得到了发展。抽象解释理论的一个有趣的特点是，在同一分析中可以将不同的领域联合收割机结合起来。事实上，抽象解释框架提供了一些标准的方法来组成抽象域，确保了保证分析可靠性所需的理论属性的保留。这些组合方法称为域细化。在（12，14）中已经给出了抽象域加细的系统处理，其中一般加细被定义为给定具体域的抽象解释的格上的下闭包算子。抽象域上的这些类型的运算符提供了高级设施，以在准确性和成本方面调整程序分析。两个最著名的域精化是析取完备化（6，9，13，15，18）和约化积（6），但它们不是唯一的。约化积可以看作是简单笛卡尔积的最精确的精化。此外，通过（6）引入了缩减的基数幂。虽然其他领域的改进，因为他们的介绍，被广泛使用和探讨，减少基数功率已经看到了明确的进一步发展，自1979年以来，除了（16）。为了验证我们的断言，我们在Google Scholar中查找了一些领域改进的科学引用（在抽象解释上下文中）的数量。我们在图1中描述了该搜索的结果。特别地，我们重点讨论了笛卡尔积、约化积和约化基数幂。这些年来，这三种情况下的引用数量都在增加，但绝对数量却有很大的不同：只要考虑到“笛卡尔积”的总引用量是964，而“约化基数幂”的引用量只有38。
interpretation (6) has been widely applied as a general technique for the sound approximation of the semantics of computer programs. In particular, abstract domains (to represent data) and semantics (to represent data operations) approximate the concrete computation. When analyzing a program and trying to prove some property on it, the quality of the result is determined by the abstract domain choice. There is always a trade-off between accuracy and efficiency of the analysis. During the years, various abstract domains have been developed. An interesting feature of the abstract interpretation theory is the possibility to combine different domains in the same analysis. In fact, the abstract interpretation framework offers some standard ways to compose abstract domains, ensuring the preservation of the theoretical properties needed to guarantee the soundness of the analysis. These compositional methods are called domain refinements. A systematic treatment of abstract domain refinements has been given in (12, 14), where a generic refinement is defined to be a lower closure operator on the lattice of abstract interpretations of a given concrete domain. These kinds of operators on abstract domains provide high- level facilities to tune a program analysis in terms of accuracy and cost. Two of the most well-known domain refinements are the disjunctive completion (6, 9, 13, 15, 18) and the reduced product (6), but they are not the only ones. The reduced product can be seen as the most precise refinement of the simple Cartesian product. Moreover, the reduced cardinal power is introduced by (6). While the other domain refinements have been, since their introduction, widely used and explored, the reduced cardinal power has seen definitely less further developments since 1979, with the exception of (16). To verify our assertion, we looked for the number of scientific citations (in the abstract interpretation context) to some domain refinements in Google Scholar. We depicted the results of this search in Figure 1. In particular, we focused on the Cartesian product, the reduced product and the reduced cardinal power. Throughout the years, the number of citations increases in all three cases, but the absolute numbers are very different: just consider that the total citations of "Cartesian product" are 964, while the ones to "reduced cardinal power" are only 38.