Ce projet implémente un algorithme de vérification de modèles basé sur la construction parallèle d'un graphe d'observation symbolique (SOG) pour la vérification de propriétés temporelles linéaires (LTL) sur des systèmes parallèles, améliorant ainsi les performances et la scalabilité de la vérification de modèles.