Making CEGAR More Efficient in Software Model Checking

Counter-example guided abstraction refinement (CEGAR) is widely used in software model checking. With an abstract model, the state space is largely reduced, however, a counterexample found in such a model that does not satisfy the desired property may not exist in the concrete model. Therefore, how to check whether a reported counterexample is spurious is a key problem in the abstraction-refinement loop. Next, in the case that a spurious counterexample is found, the abstract model needs to be further refined where an NP-hard state separation problem is often involved. Thus, how to refine the abstract model efficiently has attracted a great attention in the past years. In this paper, by re-analyzing spurious counterexamples, a new formal definition of spurious paths is given. Based on it, efficient algorithms for detecting spurious counterexamples are presented. By the new algorithms, when dealing with infinite counterexamples, the finite prefix to be analyzed will be polynomially shorter than the one dealt with by the existing algorithms. Moreover, in practical terms, the new algorithms can naturally be parallelized that enables multi-core processors contributes more in spurious counterexample checking. In addition, a novel refining approach by adding extra Boolean variables to the abstract model is presented. With this approach, not only the NP-hard state separation problem can be avoided, but also a smaller refined abstract model can be obtained. Experimental results show that the new algorithms perform well in practice.