00000cab a22000003a 4500 UP-99796217608835460 Buklod 20231007234836.0 m |o d | ta 090519s xx d | ||r ||||| || DENGII eng Tan, Jianbin Heuristic-guided counterexample search in FLAVERS. pp. 201-210 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. Software. Software engineering. Software / Program Verification. Formal methods. Validation. Model checking. Verification. FLAVERS. Counter examples. Heuristic search. Software engineering notes. 29, 6 (2004). FO UPD DENG-II Article