Skip to main content
Department of Information Technology

ProFuN Tools

Psi-calculi Workbench

Psi-calculi workbench is a parametric tool for concurrent system verification and in particular WSN like networks. It is based on the process calculi formalism and features execution and equivalence checking modules.


MPass can decide bounded-phase reachability for message passing programs. Each communicating process composing the network can alternate between sending and receiving phases a bounded number of times. Channels composing the network can be of three different semantics: lossy, stuttering or unordered, i.e. messages in the channels can be, respectively, lost, duplicated or re-arranged. MPass efficiently and uniformly reduces the bounded-phase reachability problem into the satisfiability of quantifier-free Presburger formula for each of the above mentioned semantics, thus allowing to leverage the power of SMT solvers.

Other Tools


Updated  2015-06-25 19:11:30 by Andreas Löscher.