Affinement D'Abstraction Guidé par Contre‑Exemples (CEGAR)

Un processus itératif de vérification qui alterne entre la vérification par modèle d'un système abstrait et des étapes d'affinement guidées par des contre‑exemples jusqu'à ce que la propriété soit prouvée sur le système concret ou qu'un contre‑exemple réel soit trouvé.