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.

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.

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.

In the Advanced Algorithms course we will see advanced methods of algorithmic design in different models of computation.

Some of the topics that we will see are:
* Introduction to the PRAM model (Parallel RAM)
* Parallel algorithms for the Maximum Matching problem
* Prime numbers, testing from primality, quantum algorithms for factorization
* Multiplication of polynomials and Fast Fourier Transform
* Advanced Data Structures
* Randomized Algorithms

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.

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.

Software change is inevitable due to several factors like new requirements, business environment changes, errors to be repaired, underlying technologies changes, and the performance or reliability of the system may have to be improved. When a system evolves, there are forces (obstacles) that may cause friction (slow down), even beyond the primary causes (e.g., new requirements) for which the system is evolving. These forces can be more localized/superficial (bad smells) or more pervasive/deeper (technical debt). However, identifying, addressing, and managing these forces can ensure a smoother and more effective system evolution.

In this course, we will explore approaches, challenges, and open research directions on identifying, facing, and managing these forces as part of the continuous evolution of software and, in general, development artifacts.

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.

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. 

Ontologies are explicit, formal, and shared conceptualizations of a domain of interest. Description Logics are formal languages for knowledge representation used to define ontologies. The Web Ontology Language (OWL) and its profiles are based on Description Logics. We introduce the discipline of knowledge representation and reasoning. We motivate and present the syntax and the semantics of the main Description Logics, and their computational complexity for reasoning tasks. We use Protégé for a hands-on session on semantic technologies. Additionally, we discuss selected topics that occupy researchers and practitioners in the field, e.g.: ontology-based data access, concept learning, ontology repairs, etc.

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

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

Testing is the most common method to verify the correctness of software. However, implementing test cases is a tedious and time-consuming activity. For this reason, researchers actively work on the definition of techniques for automatically generating test cases at all levels, from unit test cases to system and UI test cases. This advanced course will present techniques for the automatic generation of test cases, considering different types of tests and approaches, including recent approaches based on LLMs. Furthermore,  the course shall explore the analysis of the failures revealed by the generated test cases.

Nowadays, there are vast amounts of data available in software-related repositories, such as source control systems, defect trackers, code review repositories, app stores, question-and-answer sites, and package registries. Mining this information can help to understand software development and evolution, software users, and runtime behavior; support the maintenance of software systems; improve software design/reuse; support predictions about software development; and exploit this knowledge in planning future development. This course will provide an overview of how to conduct an Mining Software Repositories (MSR) study, including setting up a study, formulating research goals and questions, identifying repositories, extracting and cleaning the data, performing data analysis and synthesis, and discussing MSR study limitations.

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 address key non-functional properties of AI-enabled systems, e.g., fairness, sustainability, and technical debt. The course will finally engage students in discussions on the research challenges and opportunities in this field.

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.

Parameterized complexity theory is concerned with a refined analysis of computational problems. The computational effort needed to decide a problem is described by (1+k)-ary functions that depend not only on the size of problem instances, but also on k >= 1 parameters that quantify relevant structural properties of instances. Many intractable problems can be classified to be `Fixed-Parameter Tractable' (FPT) for appropriate choices of parameter(s). Such FPT problems are frequently tractable in practice for instances with small parameters.

The course is an interleaving of two parts, which focus on Algorithmic (A) aspects, and on Formal Methods (FM) viewpoints, respectively. The algorithmic part (A) covers methods for designing FPT-algorithms (kernelization, and dynamic programming with graph-width parameters). The formal methods part (FM) introduces algorithmic meta-theorems for obtaining FPT-results such as Courcelle’s theorem, and classifications of `FPT-intractability' by means of concepts from mathematical logic (the W/A-hierarchies of complexity classes based on model checking problems).

The course aims at familiarizing attendees with basic concepts of computability theory and with several diverse models of computation. Following the historical development, three classical models will be presented first: Turing machines, recursive functions, and Lambda Calculus. Subsequently, more recent models in computer science and other fields like science and biology will be explained.

The focus will be on understanding underlying intuitions rather than on exhaustively formal presentations. Specific attention will be directed to the comparison of the computational power of different models by finding, whenever possible, simulations between them, modulo `reasonable' encodings. By recognizing that some quite disparate models are computationally equally powerful, we will survey some of the ample empirical evidence that ‘computability’ is a fundamental concept, the Church-Turing Thesis: every `informally computable' function is Turing-computable (and equivalently, is definable in Lambda Calculus), modulo reasonable encodings.

Complex systems, such as autonomous driving systems (ADSs), autonomous robots, and unmanned aerial vehicles (UAVs), are often employed in safety-critical domains and, therefore, require high safety guarantees. Simulation-based testing is an effective approach to assess this type of systems in different scenarios, possibly exposing safety violations. However, the approach faces different challenges: large search spaces of the scenarios, lack of precise oracles, non-deterministic behaviours, high simulation costs, etc. The course will cover a series of simulation-based testing approaches that use metaheuristic search to effectively test these systems. Specifically, it will present:

• various coverage criteria and related test generation approaches for ADSs;

• an approach to address the oracle problem in ADS testing;

• search strategies to effectively explore the search space (e.g., based on Monte Carlo Tree Search and combinatorial testing) that allow to balance between exploration and exploitation;

• techniques to accelerate the search (e.g., surrogate models);

• methods to tackle the non-determinism of the system and of the simulators.

These approaches will be demonstrated through industrial and open-source case studies, related to autonomous driving, autonomous robots, and unmanned aerial vehicles.

This course offers a focused exploration of formal methods in software development, with some emphasis on the shift of perspectives after Peter O’Hearn’s influential paper on incorrectness logic. Instead of exploiting over-approximations to prove program correctness like done with classical formal methods, incorrectness reasoning exploits under-approximations for exposing true bugs.

The overall goal of incorrectness methods is to develop principled techniques to assist programmers with timely feedback about the presence of true errors, with few or zero false alarms.

The course will overview different approaches, like program logics, pointer analysis, and abstract interpretation, for both over- and under-approximation, as well as their combination.

The fair division framework is crucial for distributing resources among individuals with diverse preferences. Its significance has grown in recent years due to its versatility in real-world contexts. Examples include charity markets, land or assets division, public resource allocation, and so forth. With this course, we offer a review of the fair division literature distinguishing between divisible and indivisible resources. We will encompass several fairness criteria, such as envy-freeness or proportionality, and examine their existence and computation. In this journey, we will emphasize both the theoretical challenges and the algorithmic approaches for determining fair allocations."