Heuristic-guided counterexample search in FLAVERS

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. Categories and Subject Descriptors D.2.4 [Software Engineering]: So...

• Type: Conference
• Year: 2004
• Where: SIGSOFT
• Authors: Jianbin Tan, George S. Avrunin, Lori A. Clarke, Shlomo Zilberstein, Stefan Leue
• Keywords: Army Research Office, Defense/Army Research Office, Short Counterexamples, SIGSOFT 2004, Software Engineering