Outil logiciel dédié à la vérification formelle de systèmes concurrents via la construction de graphes d'observation symboliques. Il permet d'analyser des modèles complexes en exploitant des techniques de parallélisation pour améliorer l'efficacité et réduire les temps de calcul. Utilisé dans le cadre de la recherche académique en informatique théorique, notamment pour l'étude des systèmes distribués et des protocoles de communication.