ProPi is a tool that statically verifies whether message passing programs are free from deadlocks.


Propi 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.


André Camacho
Hugo Vieira


Running from Eclipse

  • An Eclipse IDE installed
Installing and using the Eclipse ProPi Plugin
  • In Eclipse go to the Help menu → Install New Software
  • In the Work with field introduce :
  • Select the SDK Feature and press Next
  • Restart Eclipse
  • Create a Project or Java Project
  • Create a file with extension “.p” and select yes when the editor asks to add the Xtext nature to your project
  • Write a program on the created file (see examples below) and press save to verify

Running from the command line

  • Download ProPi.jar
  • Create a new file with extension .p
  • Using the command type: java -jar ProPi.jar
  • Specify the specific or relative path to the communicating program file or to a folder contaning multiple program files



      • André Camacho, Tools and Techniques for the Static Verification of Progress in Communication-Centred Systems, Master’s thesis, University of Lisbon, 2014 (thesis)
      • Hugo T. Vieira and Vasco T. Vasconcelos, Typing Progress in Communication-Centred Systems, Coordination’13 Proceedings, LNCS Vol 7890:236-250, Springer, 2013 (SpringerLink, Preprint)
      • Vasco T. Vasconcelos, Fundamentals of Session Types, Information and Computation, Elsevier, 217:52-70, 2012 (ScienceDirect)