How Thorough Is Thorough Enough?

Abstraction is the key for effectively dealing with the state explosion in model-checking. Unfortunately, finding abstractions which are small and yet enable us to get conclusive answers about properties of interest is noy hard. Counterexample-guided abstraction refinement frameworks have posed to help build good abstractions iteratively. Although effective in many cases, such frameworks can include unnecessary refinement steps, leading r models, because the abstract verification step is not as conclusive as it n 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.

• Type: Conference
• Year: 2005
• Where: CHARME
• Authors: Arie Gurfinkel, Marsha Chechik
• Keywords: Abstract Verification, Abstraction Refinement Frameworks, Abstractions, CHARME 2005, Hardware