Heuristic-Guided Counterexample Search in FLAVERS

Jianbin Tan, George S. Avrunin, Lori A. Clarke, Shlomo Zilberstein, and Stefan Leue. Heuristic-Guided Counterexample Search in FLAVERS. Proceedings of ACM SIGSOFT FSE, 201-210, Newport Beach, California, 2004.

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.

Bibtex entry:

@inproceedings{TACZLfse04,
  author	= {Jianbin Tan and George S. Avrunin and Lori A. Clarke and
                   Shlomo Zilberstein and Stefan Leue},
  title		= {Heuristic-Guided Counterexample Search in {FLAVERS}},
  booktitle     = {Proceedings of {ACM} {SIGSOFT} {FSE}},
  year		= {2004},
  pages		= {201-210},
  address       = {Newport Beach, California},
  url		= {http://rbr.cs.umass.edu/shlomo/papers/TACZLfse04.html}
}

shlomo@cs.umass.edu