Outline

The major line of research of the group at the Dipartimento di Informatica, Università di Pisa, has been in the areas of Calculi, Foundational Models and Abstract Machines and Programming Languages.

• Calculi

  Research has continued on developing efficient finite-state techniques for verifying properties of history dependent process calculi (e.g. calculi for mobile processes). A prototype version of a semantic-based verification environment for the $\pi$-calculus, based on Montanari and Pistore HD-Automata has been developed. The environment supports verification of both behavioral properties (bisimulation checkers) and logical formulae (model checkers).

• Foundational Models and Abstract Machines

  The tile model relies on certain rewrite rules with side effects, called tiles, reminiscent of both SOS rules and rewriting logic rules. The tile model provides a logic of concurrent systems with conditional state changes and synchronization. The tile model has been shown to be especially useful for defining compositional models of mobile processes and causal and located concurrent systems. The tile model has been used for modelling coordination formalisms equipped with flexible synchronization primitives. The main advantage of the tile approach is the full compositionality of the underlying logic, which is able to handle computations of (nonclosed) system components as they were new rewrite rules specifying complex coordinators.

• Programming Languages

  We introduces a kernel programming language, called LLinda, which supports a programming paradigm where processes as well as data can migrate from one computing environment to another. The language is equipped with a sophisticated type system which statically checks access rights violations of mobile agents.