Suggested Topics

We are happy to support strong PhD candidates in any area of computer science.

Applicants interested in collaborating with us more closely are invited to check the following list of open PhD projects, representing some of our main current research interests.

Analysis of rollback-recovery schemas on a reversible model

Among the techniques for fault tolerant systems, recovery techniques allow a system to bring back, in case of a fault, the system to a correct state just previous to the faulty one, and to continue the execution from that one.
To formalise these systems, formal model of reversible programming language are studied.

The goal of this project is to study the relationship between existing reversible language with controlled reversibility and various rollback-recovery schemas, especially causal ones, proposed in literature.

Main referenceI. Lanese, C.A. Mezzina, A. Schmitt, and J.B. Stefani. Controlling Reversibility in Higher-Order Pi. In Proc. 22nd Int. Conf. Concurrency Theory (CONCUR), LNCS 6901, Springer, 2011.

Communication-centered programming

Computing systems are nowadays highly dependent on communication due to their distributed nature,
where interaction patterns are often highly complex and error prone. It is therefore crucial to devise programming mechanisms that focus on communication for the specification of reliable systems.
This topic concentrates in the design of programming language abstractions based on principles
such as abstraction and modularity for the development of communication-centered systems.

Main referenceHans Hüttel, Ivan Lanese, Vasco T Vasconcelos, Luís Caires, Marco Carbone, Pierre-Malo Deniélou,
Dimitris Mostrous, Luca Padovani, António Ravara, Emilio Tuosto, Hugo Torres Vieira, and Gianluigi Zavattaro. Foundations of Session Types and Behavioural Contracts, ACM Computing Surveys 49(1). 2016

Quantitative analysis of variability-intensive software systems

In variability-intensive software systems, the choice of parameters may affect both the functional and nonfunctional properties of the program. Models may help reason about features such as response time, throughput, and utilization of a system. However, typically approaches do not scale because computations are not reused across the many configurations encountered in real-world models. We wish to study effective scalable techniques to tackle these issues.

Main referenceMatthias Kowal, Max Tschaikowski, Mirco Tribastone, and Ina Schaefer. Scaling size and parameter spaces in variability-aware software performance models. Proceedings of the 30th IEEE/ACM International Conference on Automated Software Engineering (ASE 2015).

Simplification techniques for dynamical systems

Dynamical systems are widely used quantitative models in many branches of science and engineering. Unfortunately the number of equations required to describe complex real-world model is typically very large. This reduces the intelligibility of the model and poses significant computational problems for its analysis. We seek automatic techniques to simplify models in a rigorous manner.

This project may combine theoretical research, algorithm implementation, and experimental evaluation on large-scale real-world models and benchmarks.

Main referenceLuca Cardelli, Mirco Tribastone, Max Tschaikowski, and Andrea Vandin, Symbolic Computation of Differential Equivalences. Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2016).

Statistical model checking for (software) product lines

Recently, much effort is put into making formal modelling languages and related analysis techniques amenable to product lines. The challenge is to handle their inherent variability, due to which the number of possible products to be analysed may be exponential in the number of features that can be installed. We tackle this problem using efficient statistical analysis techniques like distributed statistical model checking.

We wish to further investigate on the combination of formal languages and statistical analysis techniques to provide a rich framework for the quantitative analysis of product lines.

Main referenceMaurice ter Beek, Axel Legay, Alberto Lluch Lafuente, Andrea Vandin. Statistical Analysis of Probabilistic Models of Software Product Lines with Quantitative Constraints, 19th International Software Product Line Conference (SPLC 2015).

SOS Semantics for Stochastic Calculi

We study unifying frameworks to provide operational semantics of many stochastic process algebras, including their quantitative variants useful for modeling quantitative aspects of behaviors. The model is obtained by modifying the transition relation to associate a state reachability distribution, rather than a single target state, with any pair of source state and transition label.

Main reference: Rocco De Nicola, Diego Latella, Michele Loreti, Mieke Massink, A Uniform Definition of Stochastic Process Calculi. IMT Working paper 2012

Behavioural Semantics of Quantitative Process Algebras

We study how different semantics of different models ranging from fully nondeterministic processes (LTS), fully probabilistic processes (ADTMC), fully stochastic processes (ACTMC), nondeterministic and probabilistic processes (MDP) or nondeterministic and stochastic processes (CTMDP) can be re-conducted to a unifying view. We extend this uniform treatment to behavioral equivalences and want to analyze the differences with the many known one in the literature.

Main reference: Marco Bernardo, Rocco De Nicola, Michele Loreti, A Uniform Framework for Modelling Nondeterministic, Probabilistic, Stochastic, or Mixed Processes and their Behavioral Equivalences, IMT Working paper 2012.

Design and programming principles for software ensembles

Software ensembles are a new generation of self-aware, self-adaptive, autonomic software components conceived to run over highly variable (often unpredictable) computational environments. Novel design and programming principles for the development of software ensembles need to be investigated and tailored for emerging programming languages.

Main reference: Rocco De Nicola, Gianluigi Ferrari, Michele Loreti,  Rosario Pugliese, A Language-based Approach to Autonomic Computing, FMCO 2012.

Programming abstractions for trust

Trust and reputation systems are more and more used to support decision making in e-commerce applications, as well as in other fields including ad-hoc, sensor, and P2P networks. The integration of different trust and reputation system frameworks with IT system managing and interactions needs to be investigated. The existence of many reputation systems with remarkable differences calls for frameworks for modeling, analysing, implementing and comparing them, as well for integrating them into real IT systems where trust is a critical aspect, such as cloud-based ones.

Main reference: Celestini, De Nicola, Tiezzi. Network-aware Evaluations of Reputation Systems. Technical report, IMT, 2012.

Policy-based system management

Policy-based mechanisms are increasingly used to manage different aspects of IT systems, such as access control, security, reliability or performances. There is a need to develop formal languages based on industrial standards and the corresponding reasoning tools to support the analysis of policies. Another crucial aspect to be investigated is the integration of access policies with the behavioural aspects of systems (e.g. to regulate (self-)adaptation).

Main reference: Masi, Pugliese, Tiezzi. Formalisation and Implementation of the XACML Access Control Mechanism, International Symposium on Engineering Secure Software and Systems (ESSOS), LNCS 7159, pages 60-74, Springer, 2012.