Un outil de vérification de modèles parallèles utilisant des graphes symboliques d'observation, implémenté en C/C++. Il permet de choisir entre une construction séquentielle ou parallèle et exploite les packages BuDDy et Sylvan pour représenter les agrégats de manière compacte.