Gegenbeispielgeführte Abstraktionsverfeinerung (CEGAR)

Ein iterativer Verifikationsprozess, der zwischen Model Checking eines abstrahierten Systems und Verfeinerungsschritten, die von Gegenbeispielen ausgehen, wechselt, bis die Eigenschaft entweder für das konkrete System bewiesen oder ein echtes Gegenbeispiel gefunden wird.