Abstract:
The linear pi calculus is a formal model of communicating processes that distinguishes linear channels (those that are used for one communication only) from unrestricted channels (those that can be used for any number
of communications). Many interaction patterns found in real-world programs can be modeled using linear channels. These patterns include RPC, binary sessions, bounded and unbounded buffered communications, and multiparty sessions to a certain extent.
In this seminar/demonstration I will illustrate the theoretical bases and the main features of a tool developed at the Computer Science Department of the University of Torino for the analysis of communicating processes encoded in the linear pi calculus. The tool analyses untyped processes and reconstructs the (possibly linear) types of the channels they use. Various forms of type reconstruction are supported: from the basic information about the linear or non-linear usage of channels, to binary session inference, to deadlock and lock freedom inference. During the seminar I will keep the formal details to a minimum, and will use the tool to demonstrate all these forms of analysis.