Ce projet propose un algorithme de vérification parallèle hybride pour les architectures mémoire partagée et distribuée. La vérification est effectuée simultanément avec la construction parallèle de l'espace d'états du système. L'espace d'états du système est représenté par un graphe hybride appelé Graphe d'Observation Symbolique (SOG) qui combine une représentation symbolique des nœuds (ensembles d'états uniques) et une représentation explicite des arcs. Le SOG est adapté pour préserver les formules LTL à la fois étatiques et basées sur les événements.