Education

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).

Sorting networks are very simple hardware circuits that sort inputs of fixed size n by executing a predetermined sequence of binary compare-and-swap operations. Each operation costs time and energy, and thus it is important to find sorting networks that are as small as possible. However, finding optimal sorting networks is an extremely complex problem that has only been solved for a few small values of n by ingenious combinations of combinatorial techniques, mathematical insights, and clever programming of search algorithms. If you have a background in Mathematics or Computer Science and are looking for a problem that requires a new, creative approach, then this project is for you!

SAT solving tools these days are able to prove unsatisfiability of increasingly large propositional formulas. However, they do so by applying extremely complex algorithms whose correctness it is unfeasible to verify. In order to trust their results, one needs them to output a certificate of unsatisfiability that can be efficiently verified independently. Currently, the languages for such certificates cannot support all the techniques used in SAT solving. The goal of this project is to extend certification languages to cater for hitherto unconvered techniques and develop efficient algorithms for dealing with these extensions.

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.