Capsule Reviews

Heuristic-Guided Abstraction Refinement. He, Song, Gu and Sun The paper starts from the observations that model-checking suffers from the state explosion problem when applied to largescale systems and that abstraction can solve the state explosion problem. The paper concentrates on the counterexample-guided abstraction refinement (CEGAR) and its use in hardware verification. When the counterexample is spurious (i.e. it is not a real path in the original model), the abstract model should be refined to eliminate the spurious paths. In this case, state separation creates a problem for model refinement. To solve this separation problem, the paper proposes a heuristic-guided abstraction refinement. First, the preliminaries are presented where the original non-abstracted model, the abstraction process and the counterexample-guided approach are given. Then, the state separation problem is formulated and followed by the heuristic-guided search approach that uses greedy heuristics. Two heuristics are given, both of which guide the search to the feasible solutions of the state separation problem, but one is dynamic and finds better solutions. Furthermore, an algorithm for inferring the separation set from selected samples instead of the entire set is incorporated into the heuristic approach to give an efficient sampling technique. Two heuristic solvers (one for each given heuristic) are implemented and used to run a number of Benchmarks and experiments in order to compare the two proposed heuristics and other approaches.