RECAR: Recursive Explore and Check Abstraction Refinement

 L'approche Counter-Example Guided Abstraction Refinement (CEGAR) a été un grand succès dans la vérification de modèle. Depuis lors, elle a été appliquée à de nombreux problèmes différents. Il s'avère qu'il s'agit d'une approche pratique très efficace pour résoudre le problème QBF qui est PSPACE-complet. Dans ce talk, je vous présenterai une nouvelle approche semblable à CEGAR pour aborder des problèmes PSPACE, approche que nous appelons RECAR (Recursive Explore and Check Abstraction Refinement). Je parlerai ensuite d'une instantiation du framework RECAR pour résoudre le problème de satisfiabilité en logique modale K (problème canonique PSPACE-complet). Nous avons implémentés les deux approches CEGAR et RECAR pour déterminer la cohérence d’une formule en logique modale K au sein du solveur MoSaiC. Nous avons comparé expérimentalement ces approches face aux solveurs de l'état de l’art. L'approche RECAR surpasse l'approche CEGAR sur ces problèmes et se compare favorablement aux solveurs de l'état de l'art sur les benchmarks considérés.