Education

Deployment of sophisticated distributed software applications requires a deep knowledge on the cloud infrastructure and on the application to deploy. For this reasons attempts are developed to simplify and better automate the process of deploying application (DevOps). The goal of this thesis is to enhance and develop tools (e.g., based on machine learning, local search, genetic algorithms, constraint programming) to tackle some of the computational issues for automatizing the deployment of applications in the cloud, and especially the optimization of the resource usage.

When dealing with complex problems (solving big Sudoku puzzles, assign jobs to resources, ...), one of the best possible techniques to use is to combine the strength of a portfolio of available solvers to produce a better unique solver called "portfolio solver". The goal of this thesis is to study new innovative techniques that based on machine learning and heuristics can improve the solving of complex problems, possibly improving even our own gold medals winner solver SUNNY-CP, i.e., one of the best portfolio solver for optimization problems.

Do you like (board) games? Have you ever wondered if for a particular game there is a perfect strategy that allows to maximize yours point and possibly win the game? Do you think you have a new and smart way to find good strategies? Then contact us! Working for a thesis may be as fun as playing a game.

Choreographic Programming is a new programming paradigm where programmers write specifications of how concurrent programs should interact, and then a compiler automatically generates code that is guaranteed to be correct and deadlock-free. As a young paradigm, there are a lot of useful and interesting open questions, both on the theoretical and practical levels: efficient and safe programming primitives for concurrent access to shared resources; automatic deployment of code generated from choreographies in cloud environments; specifying and proving safety properties of choreographies (e.g., liveness, security, and privacy properties); integrating choreographic programming with mainstream programming languages and frameworks; exploring the theoretical limits of choreographic programming and its relationship to standard models of computing.

Many modern digital systems (as in the Internet of Things, Industry 4.0, and Cloud Computing) are highly concurrent: they carry out multiple activities at the same time and include massive numbers of actors that communicate to exchange data, using multiple CPUs and large-scale networks. Concurrency theory offers solid methodologies to conceptualise these systems, identify problems, and support decision making. Subjects for projects range from pure theory to implementations of theoretical models: quantitative properties of concurrent systems such as availability, efficiency, performance, reliability, robustness, safety, security, survivability, and timeliness; automatic verification of security protocols; new programming approaches for concurrency (e.g., transactional memories); inductive and coinductive proof methods and their applications (e.g., for infinite behaviours, as in service-oriented systems).

Microservices are loosely-coupled software components that can be developed, evolved, and scaled independently. They represent the state of the art in distributed systems development, used by companies like Netflix, Amazon, Facebook, and Google. Programming microservices is natively supported in the programming language Jolie. We are interested in studying the microservices paradigm in general, and also in how the Jolie language can be extended with useful new features such as: testing of service systems; monitoring of protocol compliance; build a web programming framework based on microservices; native integration with other languages (e.g., Java and JavaScript); make a multi-reactor implementation of the Jolie interpreter.

Choreographic Programming is a new programming paradigm where programmers write specifications of how concurrent programs should interact, and then a compiler automatically generates code that is guaranteed to be correct and deadlock-free. As a young paradigm, there are a lot of useful and interesting open questions, both on the theoretical and practical levels: efficient and safe programming primitives for concurrent access to shared resources; automatic deployment of code generated from choreographies in cloud environments; specifying and proving safety properties of choreographies (e.g., liveness, security, and privacy properties); integrating choreographic programming with mainstream programming languages and frameworks; exploring the theoretical limits of choreographic programming and its relationship to standard models of computing.

Many modern digital systems (as in the Internet of Things, Industry 4.0, and Cloud Computing) are highly concurrent: they carry out multiple activities at the same time and include massive numbers of actors that communicate to exchange data, using multiple CPUs and large-scale networks. Concurrency theory offers solid methodologies to conceptualise these systems, identify problems, and support decision making. Subjects for projects range from pure theory to implementations of theoretical models: quantitative properties of concurrent systems such as availability, efficiency, performance, reliability, robustness, safety, security, survivability, and timeliness; automatic verification of security protocols; new programming approaches for concurrency (e.g., transactional memories); inductive and coinductive proof methods and their applications (e.g., for infinite behaviours, as in service-oriented systems).