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. Preliminary concepts of software verification, typical verification flow, common program analysis techniques, decision procedures. 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.

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.

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 and Analysis of Probabilistic Systems: Stochastic Process Algebras, Timed Automata, Markov Decision Processes, Queueing Networks. Uncertainty and Learning of quantitative properties. Guidelines on building simulation environments for Cyber-Physical Systems.

Graph mining: interpreting the past, understanding the present, imagining the future. A small world: computing and analysing the degrees of separation. A very small world: computing the diameter. Centrality measures: computing betweenness and closeness centrality. Giant components and bow-tie graphs: Kosaraju-Sharir algorithm and its applications. Link prediction: similarity-based techniques and recommendation systems. Temporal graphs.

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.

This course introduces students to data processing in Python. It first builds the necessary toolset by introducing popular Python libraries for data manipulation/visualization (NumPy, Pandas), applied to simple applications. The toolset is then applied to a more complex case study on the classification of benign and malignant breast cancer. The course concludes presenting KNIME, a popular python-integrated workflow-based language for data analysis.

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.

Introduction to simulation. Monte Carlo simulation for stochastic systems (using NumPy). Discrete-event simulation for performance and reliability (using SimPy). Agent-based simulation for multi-agent systems (using Mesa). System dynamics simulation for complex systems (using Vensim and PySD).

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

General concepts. Practical application of formal methods to software systems. Overview of some common techniques for static analysis and program verification. Typical verification flow. General-purpose decision procedures. Concurrency. Domain-specific languages. Work in progress and open problems. Practical demo sessions.

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. 

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.

The course will present state-of-the art research concerning methods for the prediction and control of performance properties of software systems, highlighting contributions regarding the analysis of paradigms for large-scale systems such as micro services and serverless architectures. 

Session types are a popular approach for the verification and specification of message-passing programs. This course introduces the syntax and semantics of a process calculus to formally reason about communicating programs, presents the binary session type system, which disciplines the communication of pairs of concurrent processes and guarantees type preservation and progress, and extends the binary session-type approach to systems of multiple (two or more) concurrent participants, by introducing multiparty session types. Examples and exercises are provided, and no prior knowledge of session types is required.

Many testing and program analysis techniques require sound and up-to-date software specifications to be  effectively applied. Unfortunately, specifications are seldom available, and when they are available they are often outdated and cannot be used to test or analyze software programs. This advanced course will present testing, debugging and repairing solutions, with specific emphasis on the ones that can exploit automatically mined specifications. The first part of the course will present several specification mining techniques that can be used to extract different kinds of behavioral models. The second part of the course will present  testing, debugging and repairing techniques with some more emphasis on the ones that exploit mined specifications.

The mutual exclusion problem; safety and liveness properties; a hierarchy of liveness properties (bounded bypass; starvation freedom; deadlock freedom. Atomic read/write registers; mutex for 2 processes (Peterson algorithm) and for n processes (generalized Peterson algorithm). From Deadlock freedom to Starvation freedom (and bounded bypass) using atomic r/w-registers. Lamport's Bakery algorithm. Mutex with specialized HW primitives (test&set; swap; compare&set; fetch&add). Mutex-free concurrency; liveness conditions (obstruction freedom, non-blocking, and wait freedom). Universal object, consensus object, and universality of consensus. Binary vs multivalued consensus. Consensus number (for atomic R/W registers, test&set, swap, fetch&add, compare&swap) and consensus hierarchy.

The course aims to explore the concept of data as a common resource that can be shared, reused, and collaboratively managed for the benefit of all. It is designed for students in the fields of computer science, social sciences, and related areas, with the aim of creating cross-disciplinary contamination and uniting knowledge. The course will cover a range of topics, including open data, dataspace, civic hacking, and data visualization with the goal to delve into the importance of open data in promoting transparency and innovation, the impact of dataspace on data sharing and collaboration, and the role of civic hacking in promoting social change and citizen engagement. In addition to theoretical knowledge, the course includes a hands-on data visualization lab in the final session. This lab will enable participants to develop practical skills in creating value from data. By the end of the course, participants will have a deep understanding of the potential of data as a commons and the skills needed to create value from it.

Recent years have witnessed tremendous progress in the field of Machine Learning (ML). However, many of the recent breakthroughs demonstrate phenomena that lack explanations, and sometimes even contradict conventional wisdom. One main reason for this is because classical ML theory adopts a worst-case perspective which seems too pessimistic to explain practical ML: in reality data is rarely worst-case, and experiments indicate that often much less data is needed than predicted by traditional theory. In this series of talks we will discuss two variations of classical learning theory. These models are based on a distribution- and data-dependent perspective which complements the distribution-free worst-case perspective of classical theory, and is suitable for exploiting specific properties of a given learning task. A common theme of these models is their combinatorial nature. This can be seen as a continuation of the fruitful link between machine learning and combinatorics, which goes back to the discovery of the VC dimension more than 50 years ago.

This advanced course will cover the theory of mechanism design for single-parameter settings, with a focus on optimizing social welfare and revenue in auctions. Applications to sponsored search will also be discussed. Then, the design principles for designing simple but approximately optimal auctions will be explored.

Parameterized complexity theory aims at a refined analysis of computational problems. An instance of a problem is not only measured by its size, but also by a natural-number parameter that classifies its inner structure. Many intractable problems are `fixed-parameter tractable', which can mean that they are tractable in practice for small-parameter instances. 

The course treats Algorithmic aspects (A) and Formal-Methods viewpoints (FM) of parameterized complexity. In (A) we focus on definitions/basic properties, kernelization, dynamic programming with graph-width parameters, and in (FM) on Courcelle's Theorem for obtaining fpt-results by expressing problems as logical formulas, and the W/A-hierarchies of complexity classes based on model checking problems.

Basic probabilistic modeling using Discrete-Time Markov Chains (DTMCs) and the PRISM modeling language. Specification of system properties with Probabilistic Computation Tree Logic (PCTL). Interactive simulation and checking of system properties using the PRISM tool. Concurrency in PRISM and model checking of reward-based properties.

Introduction to robotics - basic functionalities. Architectures for autonomous robots. Software engineering in robotics and research directions.

Modern software systems are complex, heterogeneous. and open systems that require sophisticated approaches for the generation of test cases and the analysis of failures. This advanced course will cover some key cases and domains, including testing software in the field within its operational environment, testing and analysing failures of Cyber-physical Systems (CPS), testing Web applications, and detecting failures with program oracles. The course shall include a lab on Web testing.

Domain-specific languages (DSLs) assist a software developer (or end-user) in writing a program using idioms similar to the abstractions found in a specific problem domain. Indeed, the enhanced software productivity and reliability benefits that have been reported from DSL usage are hard to ignore, and DSLs are flourishing. However, tool support for DSLs is lacking when compared to the capabilities provided for standard General-Purpose Languages (GPLs). For example, support for unit testing of a DSL program, as well as DSL debuggers, is rare. A Systematic Mapping Study (SMS) has been performed to better understand the DSL research field and to identify research trends and any possible open issues. This course introduces students to appropriate methodologies and tools needed to support the development of DSLs. Open problems in DSLs are discussed as well.

This course aims to introduce the fundamentals for creating adequate experience for the user, by means of basic design principles, ways to generate ideas, and how to develop proper interfaces. This introductory course is composed of theoretical classes with practical examples of application, such as usability and rapid prototyping, wire-frames, and principles of design.