How Thorough is Thorough Enough?
Abstract
Abstraction is the key for effectively dealing with the state
explosion problem in model-checking. Unfortunately, finding
abstractions which are small and yet enable us to get conclusive
answers about properties of interest is notoriously hard.
Counterexample-guided abstraction refinement frameworks have been
proposed to help build good abstractions iteratively. Although
effective in many cases, such frameworks can include unnecessary
refinement steps, leading to larger models, because the abstract
verification step is not as conclusive as it can be in theory.
Abstract verification can be supplemented by a more precise but much
more expensive thorough check, but it is not clear how often
this check really helps. In this paper, we study the relationship
between model-checking and thorough checking and identify practical
cases where the latter is not necessary, and those where it can be
performed efficiently.