Heuristic-Guided Counterexample Search in FLAVERS
Jianbin Tan
George S. Avrunin
Lori A. Clarke
Shlomo Zilberstein
Stefan Leue
Abstract
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.
Download
[pdf]