Counterexample-Guided Abstraction Refinement

An iterative verification process that alternates between model checking of an abstracted system and refinement steps driven by counterexamples until either the property is proved on the concrete system or a genuine counterexample is found.