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.

TBA

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.

This course introduces models of concurrent and distributed programming. The course will explore this topic presenting different paradigms of coordination of concurrent and distributed systems (including shared-memory, message-passing, and tuple spaces) as well as related linguistic constructs. The theoretical underpinning will be reinforced by showing how popular programming languages feature concurrency.

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.

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. 

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

This course will discuss challenges and key techniques to enhance the security of software systems. Topics will include: The role of software vulnerabilities in cybersecurity. The most common classes of software vulnerabilities. Vulnerability disclosure and management. Vulnerability assessment through fuzzing and static analysis. The Secure Software Development Lifecycle. Software Supply Chain Security.

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.

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.

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

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.

TBA