Ph.D. Program

Basic notions of algorithms and complexity; Divide-and-Conquer; Dynamic Programming; Basic data structures: heaps, hash tables; Greedy; Local Search; Network Flow; All-pairs Shortest Paths; NP-complete problems and intractability; PSPACE

Basics on formal models of (concurrent) computations, operational semantics and (labelled) transition systems, regular expressions, basic process algebras. Notions of propositional and predicate logic, Boolean satisfiability and satisfiability modulo theories, applications to verification problems. Basic concepts of software modelling and analysis with stochastic processes, discrete-time markov processes, and petri nets.

Basic concepts of software development paradigms, application domains, the software life cycle, design of software systems and modeling, software architectures. The course also provide some basic knowledge of the tools used to generate software programs from models.

How to write a paper. How to give a scientific talk. How to referee a scientific paper.

An overview of the teaching part of the course and the support that the group offers to students

Basic notions of equilibrium: dominant versus Nash; computational issues of equilibria; performance of equilibria (price of stability and anarchy). Congestion games: congestion games, cost sharing games, load balancing; price of anarchy and stability; PLS-completeness; speed of convergence. Mechanism design and strategyproofness in coalition games. Learning in coalition games.

Introduction to linear programming; the set cover problem; greedy algorithms and local search; rounding data and dynamic programming; deterministic rounding of linear programs; random sampling and randomized rounding of linear programs; the primal-dual method; techniques to prove the hardness of approximation.

The course will discuss the motivation for self-adaptation, the basic principles and system properties of autonomous and self-adaptive systems and how to engineer these kinds of systems. The course will also present concrete systems in the domain of e-Health, smart mobility, robotics, and recent advances in the literature.

This course is about theory of distributed computing. We will learn about some of the most studied models of distributed computing, with focus on synchronous and fault-free models. We start from the basics: we formally define the distributed setting and what is a distributed algorithm, illustrating the formal definition with some simple examples. Then we slowly build up on this, focusing at the beginning on simple networks such as rings, and learning how to solve, in this setting, simple fundamental tasks such as coloring, maximal independent set, and maximal matching. Next, we will discuss the topic of decidability: given a problem, can we automatically decide what is its asymptotic distributed complexity? We will see that for a large class of problems, on ring networks, this is actually possible. After that, we switch to more general network topologies, and we will see how to solve some tasks in this setting. Finally, we will see some impossibility results. In particular, we will see how to prove lower bounds for the distributed complexity of some classical problems. A basic knowledge about graph theory and big-O notation is assumed.

Modern systems are becoming more and more human-centric and smart. In this course we will explore approaches, challenges, and open research directions in the engineering of human-centric and smart systems. We will give special attention to quality aspects, but also to values that are important to take into account when humans are involved not only as users but also as entities in the decision-making loop.

Ethical algorithm design. Basics of machine learning. Algorithmic privacy. Algorithmic fairness. Explainability of supervised machine learning. Algorithmic robustness.

Modelling, analysis, and testing of probabilistic systems: Stochastic Process Algebras, Markov Decision Processes, Timed Automata, Queueing Networks. Software Performance: uncertainty and learning of quantitative software properties.

Preliminary notions of cryptography and distributed systems. Consensus in distributed systems. Bitcoin blockchain and contracts. Ethereum blockchain and contracts. Vulnerabilities of smart contracts. Formal methods for smart contracts.

Modelling of reactive systems, review of the model checking approach, temporal logics (LTL, CTL, and CTL*), safety and liveness properties of reactive systems, fairness conditions.

This course introduces the notion of Boolean Satisfiability (SAT) and Satisfiability Modulo Theories (SMT). The course will provide an overview of decision procedures and it will be mainly concerned with the implementation and the application of SAT and SMT to concrete problems. The course will cover the issue of encoding problems into appropriate SAT and SMT instances, and it will present examples from various research and industry domains, exploring the solutions currently available.

General concepts and techniques of software testing. Main concepts of dependability and reliability testing. Most interesting research challenges in software testing.

This course will explore model-driven Engineering methodologies applied to practical case studies.The course will cover the basic knowledge of modeling, metamodeling, transformations, and code generation. 

Experimental design; Measures in algorithmic experiments; Algorithm and code tuning; Building test environments; Analysis of experimental data.

The focus will be on fixed-parameter tractability results for graphs of bounded width (path-, tree-, clique-width) that can be obtained both by algorithmic techniques (dynamic programming) and by formal-method techniques (logical meta-theorems).

Motivation and regulations for (cyber)security; Preliminary concepts; Coding standards and vulnerability databases; Examples.