Lazy Shape Analysis
Lazy Shape Analysis
复制标题
惰性形状分析
DOI：
10.1007/11817963_48
复制
发表时间：
2006
期刊：
影响因子：
--
通讯作者：
Grégory Théoduloz
中科院分区：
文献类型：
--
作者：
Dirk Beyer;T. Henzinger;Grégory Théoduloz
许多软件模型检查器是基于谓词抽象的。如果验证目标依赖于指针结构，那么这种方法就不能很好地工作，因为很难为堆找到适当的谓词抽象。相反，使用基于图的堆抽象的形状分析可以提供递归数据结构的紧凑表示。我们将形状分析集成到软件模型检查器Blast中。因为形状分析是昂贵的，我们不应用它全局。相反，我们确保像谓词一样，形状图只在证明验证目标所需的地方计算和存储在本地。为了实现这一点，我们将惰性抽象细化（迄今为止仅用于谓词抽象）扩展到三值逻辑结构。这种方法不仅提高了模型校核的精度，而且提高了形状分析的效率。我们通过扩展Blast来实现对Tvla的调用。
Many software model checkers are based on predicate abstraction. If the verification goal depends on pointer structures, the approach does not work well, because it is difficult to find adequate predicate abstractions for the heap. In contrast, shape analysis, which uses graph-based heap abstractions, can provide a compact representation of recursive data structures. We integrate shape analysis into the software model checker Blast. Because shape analysis is expensive, we do not apply it globally. Instead, we ensure that, like predicates, shape graphs are computed and stored locally, only where necessary for proving the verification goal. To achieve this, we extend lazy abstraction refinement, which so far has been used only for predicate abstractions, to three-valued logical structures. This approach does not only increase the precision of model checking, but it also increases the efficiency of shape analysis. We implemented the technique by extending Blast with calls to Tvla.