Refinamiento de Abstracción Guiado por Contraejemplos (CEGAR)

Un proceso iterativo de verificación que alterna entre el model checking de un sistema abstraído y pasos de refinamiento impulsados por contraejemplos hasta que la propiedad se prueba en el sistema concreto o se encuentra un contraejemplo genuino.