ProPi is a tool to statically verify whether message passing programs are free from deadlocks. The tool takes as input a system specified in the pi-calculus, together with typing annotations that describe the communications in the channels, as well as event annotations so as to capture the overall ordering of the communications. The tool produces as result either a positive answer (the system type checks), in which case the properties of protocol fidelity (system communications follow the typing prescription) and progress (deadlock absence) hold. Otherwise, the system exhibits error information so as to allow to identify what is the problem in the system specification. The tool includes an Eclipse plugin and a standalone command line interface.
