Heuristic-guided counterexample search in FLAVERS
Heuristic-guided counterexample search in FLAVERS
复制标题
DOI：
10.1145/1029894.1029922
复制
发表时间：
2004-10
期刊：
影响因子：
--
通讯作者：
Jianbin Tan;G. Avrunin;L. Clarke;S. Zilberstein;S. Leue
中科院分区：
文献类型：
--
作者：
Jianbin Tan;G. Avrunin;L. Clarke;S. Zilberstein;S. Leue
有限状态验证（FSV）工具（如模型检查器）的一个好处是，当属性无法验证时，可以提供一个反例。然而，并非所有的反例对试图理解和定位故障的分析师都同样有用。反例通常很长，很难理解。因此，重要的是FSV工具找到短的反例，并迅速做到这一点。常用的搜索策略，如广度优先和深度优先搜索，通常在这两个方面都表现不佳。在本文中，我们研究了启发式搜索策略的FSV工具FLAVERS，并提出了一种新的两阶段反例搜索策略。我们描述了一个实验表明，这两个阶段的策略，结合适当的questionistics，是非常有效的快速找到一个大的验证问题集短的反例。
One of the benefits of finite-state verification (FSV) tools, such as model checkers, is that a counterexample is provided when the property cannot be verified. Not all counterexamples, however, are equally useful to the analysts trying to understand and localize the fault. Often counterexamples are so long that they are hard to understand. Thus, it is important for FSV tools to find short counterexamples and to do so quickly. Commonly used search strategies, such as breadth-first and depth-first search, do not usually perform well in both of these dimensions. In this paper, we investigate heuristic-guided search strategies for the FSV tool FLAVERS and propose a novel two-stage counterexample search strategy. We describe an experiment showing that this two-stage strategy, when combined with appropriate heuristics, is extremely effective at quickly finding short counterexamples for a large set of verification problems.