piexplorer : an explicit state-space generation tool and a model-checker for the Pi-calculus

Team : APR

The problem of generating an explicit state-space for the pi-calculus is a complex problem. As of today, there exists only two tools with this functionality : the HAL laboratory and pi-explorer. The latter is based on a symbolic semantics that is much more economical than the early semantics as implemented by HAL. A model checker is also associated to the tool, but it is possible to use external tools based on the state graphs generated by the pi-explorer. These tools are based on recent works of the APR team (the pi-graphs), in a collaboration with university of Evry and université libre de Bruxelles.

Software leader : Frédéric PESCHANSKI