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.

Principio

Utilizar los contraejemplos producidos a nivel abstracto para distinguir comportamientos espurios de errores reales y refinar la abstracción solo cuando sea necesario, intercambiando alarmas falsas inducidas por la abstracción por aumentos dirigidos de precisión.

Demostración

Verificar una propiedad de seguridad de un componente de software mediante una abstracción por predicados; si el verificador devuelve un contraejemplo, simularlo en el programa concreto. Si la simulación muestra que la traza es espuria, añadir predicados que separen el camino espurio y repetir la verificación hasta que la propiedad se cumpla o aparezca una traza fallida real.

Aplicación incorrecta

Tratar todo contraejemplo como real sin comprobar su naturaleza espuria, aceptando falsos negativos, o añadir repetidamente predicados que eliminan trazas espurias pero provocan una explosión del espacio de estados y pérdida de escalabilidad.

Consecuencia

Con una abstracción sonora y heurísticas de refinamiento adecuadas, el método suele producir o bien una prueba de corrección en un modelo abstracto compacto o bien un contraejemplo concreto; en la práctica puede mejorar drásticamente la escalabilidad frente a métodos basados en estados concretos.

Inversión

Un enfoque puramente abstracto que nunca refina según contraejemplos (abstracción de una sola pasada) o la búsqueda exhaustiva en el espacio de estados concretos sin abstracción; ambos extremos generan o bien alarmas espurias persistentes o bien no escalan.

Límite

Se aplica cuando puede definirse un modelo abstracto y una estrategia de refinamiento; no garantiza terminación para todos los sistemas (por ejemplo, algunos sistemas de estados infinitos o esquemas de refinamiento mal elegidos) y su eficacia depende de la expresividad de los predicados o primitivas de refinamiento disponibles.

Tensión semántica

Entre precisión y escalabilidad: abstracciones más fuertes aumentan la escalabilidad pero generan más contraejemplos espurios; un refinamiento agresivo reduce la espuriedad pero corre el riesgo de una explosión combinatoria.

Síntesis

CEGAR es un bucle cerrado de verificación: abstraer, comprobar, analizar el contraejemplo, refinar la abstracción para eliminar comportamiento espurio y repetir hasta obtener una prueba o un contraejemplo concreto, equilibrando solidez, precisión y límites de recursos mientras se reconoce la posible no terminación en casos patológicos.