几个基于图的关系数值抽象域
A Few Graph-Based Relational Numerical Abstract Domains
摘要:
本文给出了一类非关系数值抽象域的系统设计。构造的域表示形式为(C中的vj - vi)的不变量的集合,其中vj和vi是两个变量,并且C存在于P(Z)、P(Q)或P(R)的抽象中。我们称这类域为弱关系域。允许这种建设的基本概念是潜在的图形和最短路径封闭算法在exotic-like代数的扩展。给出了示例构造,以检索知名的域以及新的。这样的域可以在抽象解释框架中使用,以便设计各种静态分析。这种结构的一个主要好处是它的模块化,允许快速实现新的抽象域从现有的。
英文摘要:
This article presents the systematic design of a class of relational numerical abstract domains from non-relational ones. Constructed domains represent sets of invariants of the form (vj - vi in C), where vj and vi are two variables, and C lives in an abstraction of P(Z), P(Q), or P(R). We will call this family of domains weakly relational domains. The underlying concept allowing this construction is an extension of potential graphs and shortest-path closure algorithms in exotic-like algebras. Example constructions are given in order to retrieve well-known domains as well as new ones. Such domains can then be used in the Abstract Interpretation framework in order to design various static analyses. Amajor benfit of this construction is its modularity, allowing to quickly implement new abstract domains from existing ones.
机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。