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.

How to do scientific communication

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.

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.

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. 

Uncertainty-wise CPS Modeling, Evolution, and Testing (Uncertainty modeling, Uncertainty and model evolution, Uncertainty-wise testing and optimization). Digital Twins based CPS Analyses (Introduction to digital twins, Advanced analyses with digital twins, Digital twin evolution). Quantum Computing for CPS Analyses (A brief introduction to quantum computing, Example applications). 

This course aims at rekindling the historical connection between neuroscience and computer science, exploring some of the algorithmic principles that underlie both brains and machines. Pioneering figures like von Neumann and Turing recognized this deep link, and we'll delve into the computational core of fundamental questions in neuroscience. We'll examine how neurons process information, leverage intricate connections, and potentially inspire new computational frameworks. By exploring how these biological algorithms underlie perception, action, and even language, we'll bridge the gap between brain and computation.

This course will investigate the following research question: can quantum computation and communication speed up distributed networks? This question is directly related to the limits of distributed computation. The classical limits of distributed computation are well-known today, most of which are captured by the LOCAL model of computing. We will explore its quantum (and super-quantum) counterparts and present techniques to bound possible quantum advantage.

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

This course aims at rekindling the historical connection between neuroscience and computer science, exploring some of the algorithmic principles that underlie both brains and machines. Pioneering figures like von Neumann and Turing recognized this deep link, and we'll delve into the computational core of fundamental questions in neuroscience. We'll examine how neurons process information, leverage intricate connections, and potentially inspire new computational frameworks. By exploring how these biological algorithms underlie perception, action, and even language, we'll bridge the gap between brain and computation.

Concurrent and distributed software is nowadays pervasive to most computing devices. However, it is particularly difficult to design and validate. Concurrency bugs appear frequently and have a substantial impact, as not only they may affect many people, but also may cause a severe financial damage. There is thus a pressing need of using rigorous approaches and tools to specify and verify such systems. Industrial actors like Amazon, Facebook, Google, IBM, Intel, Microsoft, or NASA, just to name a few, are using tools to formally guarantee that (parts of) their software is bug-free.

This course covers basic principles, techniques, and some tools to help on the challenging task of developing concurrent software systems. This involves understanding languages to specify systems and their properties. There are various kind of key properties of concurrent systems; we will focus on basic safety and liveness properties, which are enough to express functional requirements of concurrent and distributed algorithms.

Note - all lectures have a companion list of suggested exercises (and I am available in office hours to help with them and provide feedback about your solutions).

Lecture 1: concurrent reactive systems

- requirements to model concurrent reactive systems

- the calculus of communicating systems (syntax and operational semantics)

- motivating and illustrative examples

Lecture 2: equivalences for CCS

- requirements for an equivalence notion

- basics on co-induction

- observational behavioural equivalence (axiomatically and co-inductively)

Lecture 3: the pi-calculus

- why do we need a dynamic process topology?

- the pi-calculus

- early and late operational semantics

- early and late bisimulations

- motivating and illustrative examples

Lecture 4: (mobile) modal logics

- Hennessy-Milner Logic

- the mu-calculus

- tools for reasoning about process behaviour

Lecture 5 (optional): research topics

- static analysis

- expressiveness

- protocol soundness

Normative requirements elicitation and specification, Formal semantics of normative rules, Conflict detection in normative rulesets, Redundancy detection in normative rulesets, Normative requirements verification of autonomous systems.

Normative requirements elicitation and specification, Formal semantics of normative rules, Conflict detection in normative rulesets, Redundancy detection in normative rulesets, Normative requirements verification of autonomous systems.

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.

High-level Intro; Basics of Reversible Computing; Basics of Quantum Computing; Deutsch-Jozsa Algorithm; Grover's Algorithm; Quantum Complexity.

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

The course aims at providing students with a gentle introduction to the intersection of software engineering (SE) principles and artificial intelligence (AI) technologies. In the first part, the course will target SE with AI, introducing the key elements to design an AI-based technique for SE, other than the multiple ways AI can be used to assist software engineers in practice. In the second part, the course will target SE for AI, providing insights on how software engineering principles, standards, and instruments might help addressing key non-functional properties of AI-enabled systems, e.g., fairness, sustainability, and technical debt. The course will finally engage students in discussions on exemplary cases coming from the scientific literature. 

In this research-oriented course, we will study cognitive robots capable of physically interacting with their environment, collaborating with humans and other agents, and autonomously performing a variety of tasks in complicated environments. The general theme of the course is the overall objective of making cognitive robots act in a transparent manner that makes sense to humans and other agents, and can function reliably over a long period of time. To this end, we will introduce and exemplify the desirable cognitive capabilities required to realize cognitive robots, such as the means for representing and reasoning about scenes in virtual and real environments. In the main part of the course, we will study novel methods, concepts, and tools to support the automated engineering of robotic agents, covering their complete lifecycles in virtual and real environments. We will present tools and methods to enable humans to specify, construct, validate, and evaluate these systems as the robots themselves to autonomously adapt their software to the various and changing runtime requirements induced by the robot’s task or environment.

A temporal graph is a graph modeling the dynamic nature of its links and of its nodes, meaning that it exists through (a discrete-labeled) time and, at each timestamp, only a subgraph of the base graph is active. Despite being around for more than three decades, only recently this structure has received more attention from the community, and in particular from the theoretical community. Such interest can be felt through the many recent papers on the subject, as well as through the inauguration of two specialized events (a satellite ICALP workshop and the conference SAND). With the main objective of stimulating the research on the field, we propose a course where we will learn about these structures, with particular interest on recent theoretical results about connectivity-related problems.

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.

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.