一种新的基于差界矩阵的数值抽象域
A New Numerical Abstract Domain Based on Difference-Bound Matrices
摘要：
本文通过抽象解释提出了一种新的静态分析数值抽象域。这个域允许我们表示形式为（x-y<=c）和（+/-x<=c）的不变量，其中x和y是变量值，c是整数或实常数。抽象元素用差分定界矩阵表示，广泛应用于模型检查器，但我们必须设计新的操作符来满足抽象解释的需要。其结果是一个完整的无限高的晶格具有扩大，缩小和共同的传递函数。我们专注于给出一个有效的O（n2）表示和基于图的O（n3）算法-其中n是变量的数量|并声称该域总是比公知的区间域执行得更精确。为了说明这个领域的精度/成本权衡，我们已经实现了简单的抽象解释器玩具命令和并行语言，使我们能够证明一些非平凡的算法正确。
英文摘要：
This paper presents a new numerical abstract domain for static analysis by abstract interpretation. This domain allows us to represent invariants of the form (x-y<=c) and (+/-x<=c), where x and y are variables values and c is an integer or real constant. Abstract elements are represented by Difference-Bound Matrices, widely used by model-checkers, but we had to design new operators to meet the needs of abstract interpretation. The result is a complete lattice of infinite height featuring widening, narrowing and common transfer functions. We focus on giving an efficient O(n2) representation and graph-based O(n3) algorithms - where n is the number of variables|and claim that this domain always performs more precisely than the well-known interval domain. To illustrate the precision/cost tradeoff of this domain, we have implemented simple abstract interpreters for toy imperative and parallel languages which allowed us to prove some non-trivial algorithms correct.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
