Davide Sangiorgi

My main research area is concurrency theory, with a special interest
for distributed systems. I try to develop models and techniques for
the analysis, specification, and verification of software for such
systems. For this, I make use of process calculi, modal and temporal
logics, theories of behavioural equivalence among processes, type
systems. I study models also as a basis for the design of new
programming language construct for concurrent or distributed systems.




In a theory of concurrency for process mobility the development of
behavioural equivalences (and equational theories) is fundamental,
because these theories represent an essential ingredient for the
design of methods and techniques for the specification and the
verification of various important properties, such as the security of
the information flow, authentication, program transformations aiming
at improving the efficiency of the code. They are also essential in
the study of the expressiveness of different formalisms. In the case
of distributed systems and in higher-order concurrency (where parts of
the code, or processes, may be copied and/or these theories remain
today not fully understood and offer serious technical
challenges. Even minimal forms of mobility create surprising
difficulties in the (inductive or coinductive) definition of simple
behavioral equivalences. Other difficulties arise when one tries to
use type system to discipline the behaviour of the processes.

I use modal and temporal logics for distributed systems
that allow us to describe not only behavioural properties of the
systems, but also topological structures.
We study the expressiveness and the decidability of such logics,
trying to isolate the most useful basic constructs and operators.
The objective is then to develop more abstract idioms, that can be
expressed in the basic logic but are easier to use,
and associated proof techniques and tools.


During the last few years, issues related to the control of resources
and mobility, in various forms, have been a central theme in the
research area of type systems. The types allow us to express important
guarantees on the possible behaviour of the processes. I have been
active in this area since 1993. Examples of type systems that we have
designed include: types for the control of the access rights to
resources; types for the control of the distribution of resources in a
system, types for the control of the interferences among processes,
types for the control of the mobility of the processes (where the
permissions for the mobility are expressed through the types), types
that guarantee the secrecy of the communications among processes.
More recently, I have been involved in applications of process calculi
in Service-Oriented Computing.  This is an emerging paradigm for
distributed systems in which services are used as single computing
units.  Services are autonomous entities, independent from the
platform in which they may be described, and programmed so to obtain
networks of distributed applications within a single organisation and
allowing different organisation to cooperate. Finally I am interested
in the use of process calculi and algebras for the analysis of complex
systems, such as biological systems: defining their semantics, and
developing techniques for their verification and simulation.  Process
calculi and algebra allow us to master such complexity for two main
reasons. The first reason is that these models allow us to abstract
away from the internal structure of the sub-systems. The second reason
has to do with the compositionality properties of these models, which
allow us to describe the behaviour of a system starting from the
descriptions of its components (the subsystems).