Heuristic-Guided Abstraction Refinement
F. He, Xiaoyu Song, M. Gu, Jian Sun · The Computer Journal · 2007
Model checking has been considered as a promising approach to establish the correctness of systems. Counterexample-guided abstraction refinement is a key strategy for model checking in verification of large-scale systems. State separation problem poses the main hurdle during the refinement. We present two fast heuristics to solve this problem. We prove the effectiveness of our heuristics by both theoretical analysis and experimental results. Experimental results show the promising performance of our approach.