Symbolic Localization Reduction with Reconstruction Layering and Backtracking
Symbolic Localization Reduction with Reconstruction Layering and Backtracking
复制标题
通过重建分层和回溯减少符号定位
DOI：
--
复制
发表时间：
2002
期刊：
影响因子：
--
通讯作者：
Anna Gringauze
中科院分区：
文献类型：
--
作者：
S. Barner;D. Geist;Anna Gringauze
降低定位是用于模型检查的抽象再填充方案，该方案是由Kurshan [12]引入的，作为解决状态爆炸的一种手段。它是完全自动的，但是尽管已经完成了与该方案相关的工作，但它仍然具有计算复杂性。在本文中，我们介绍了减少本地化的算法改进，这使我们能够克服其中一些问题。也就是说，我们提出了一种用于路径重建的新符号算法，包括增量和回溯。我们已经实施了这些改进，并将它们与以前的许多工业示例进行了比较。在某些情况下，改进是巨大的。使用这些改进，我们能够验证以前无法解决的电路。
Localization reduction is an abstraction-refinement scheme for model checking which was introduced by Kurshan [12] as a means for tackling state explosion. It is completely automatic, but despite the work that has been done related to this scheme, it still suffers from computational complexity. In this paper we present algorithmic improvements to localization reduction that enabled us to overcome some of these problems. Namely, we present a new symbolic algorithm for path reconstruction including incremental refinement and backtracking. We have implemented these improvements and compared them to previous work on a large number of our industrial examples. In some cases the improvement was dramatic. Using these improvements we were able to verify circuits that we were not previously able to address.