piexplorer : un générateur d'espace d'état explicite et un vérificateur de modèle pour le Pi-calcul

Équipe : APR

La génération d'espace d'états pour le pi-calcul est un problème complexe. Il n'existe à ce jour que deux outils offrant cette fonctionalité : le laboratoire HAL et pi-explorer. Ce dernier repose sur une sémantique symbolique beaucoup plus économe que la sémantique précoce exploitée par HAL. Un vérificateur de modèle est associé à l'outil, mais il est possible d'utiliser d'autres outils à partir du graphe d'état généré en sortie de pi-explorer. Ces outils sont basés sur des travaux récents de l'équipe APR (les pi-graphes) en collaboration avec l'université d'Evry et l'université libre de Bruxelles.

Responsable : Frédéric PESCHANSKI
https://github.com/fredokun/piexplorer
Mentions légales
Carte du site