My research activity in the field of formal methods in computer science is aimed at the development of methodologies for the design of computer, communication and software systems on the basis of the following principles:

• Formality: the utilization of rigorous mathematical foundations for defining modeling languages, so as to avoid ambiguity and enable system description analysis and system property prediction.
• Expressiveness: the capability of easily representing computation and communication activities as well as functional and nonfunctional system aspects.
• Usability: the provision of abstractions related to paradigms, patterns, and styles frequently occurring in the system development practice, while hiding technical details.
• Efficiency: the automation of the system development process for synthesizing systems from their formal descriptions by preserving the properties verified on the latter.

The ultimate goal of my research activity is to increase system quality in terms of dependability and performance and, at the same time, reduce system development and maintenance costs deriving from the late discovery of errors.

The process algebraic architectural description language Æmilia and the companion verification tool TwoTowers, together with a number of methodologies described in the book "A Process Algebraic Approach to Software Architecture Design".

• Semantics of concurrent programming languages.
• Process calculi, behavioral equivalences, and modal logics.
• Modeling and verification of concurrent and distributed systems.
• Performance evaluation of computer systems and networks.
• Foundations of software architecture and engineering.
• Automated support for model-driven software development.

• PaCo - Performability-Aware Computing: Logics, Models, and Languages [2008-2010]
  (funded by the Italian Ministry for Education, University and Research under programme PRIN).