Computer Science and Systems Engineering

Research Topics in Computer Science

The goal of this course is to get students acquainted with research methods in computer science, including publication strategies and a classification of its main outlets (workshops, conferences, and journals). Students will receive a broad perspective on the major sub-fields computer science (e.g., programming languages, verification, software engineering, security, ?) by means of guest lectures delivered by leading experts in the respective areas.

Qualitative and Quantitative Formal Methods for Computer Science

This course offers an introduction to core topics in formal methods for the specification and analysis of systems, both for functional and nonfunctional properties. Students will be exposed to basic models of computation such as labelled transition systems and process algebra, formal approaches to specifying the semantics of programming languages (such as operational and denotational semantics), and quantitative analysis methods based on Markov processes.

Probabilistic and Stochastic Model Checking

Model checking is an automated formal verification technique whose main idea is to formally specify both the system specification and its properties (typically, by means of temporal logic) and automatically verify that such properties are satisfied (or to which extent they are). This course aims at presenting the fundamentals of model checking techniques for the verification of distributed and concurrent systems. Different classes of temporal logics will be introduced that rely on the use of semantic models to provide a logical framework for the analysis and verification of complex systems.

Principles of Concurrent and Distributed Programming

The course objective is to introduce the basics of concurrent programming problems through an illustration of the concepts and techniques related to modeling systems in which there are more components that are simultaneously active and need to coordinate and compete for the use of shared resources. At the end of the course the student will have a good understanding of the constructs for concurrent programming and be able to use them to write and analyze concurrent programs.

Optimal Control

Discrete-time optimal control: dynamic programming for finite/infinite horizon and deterministic/stochastic optimization problems. LQ and LQG problems, Riccati equations, Kalman filter. Deterministic continuous-time optimal control: the Hamilton-Jacobi-Bellman equation and the Pontryagin?s principle. Examples of optimal control problems in economics.
An economic application of optimal control: a dynamic limit pricing model of the firm.

Prerequisites: Matrix Algebra

Modelling and Verification of Reactive Systems

Computing systems are becoming increasingly sophisticated and control key aspects of our lives. In light of the increasing complexity of such computing devices, one of the key scientific challenges in computer science is to design and develop computing systems that do what they were expected to do, and do so reliably. The aim of this course is to introduce models for the formal description of computing systems, with emphasis on parallel, reactive and possibly real-time systems, and the techniques for system verification and validation that accompany them.

Model Predictive Control

Quick review of linear dynamical systems in state-space form, stability, state-feedback control and observer design, linear quadratic regulation and Kalman filtering. Basic model predictive control (MPC) algorithm and the receding horizon principle. Linear MPC: formulation, quadratic programming, stability properties. Multiparametric programming and explicit MPC. MPC of hybrid dynamical systems subject to linear and logical constraints. Stochastic MPC. Selected applications of MPC to automotive and aerospace systems, supply chains, financial engineering.


The course covers the fundamentals on modelling heterogeneous materials with periodic, quasi-periodic or non-ordered microstructures. Metamaterials, auxetic materials, chiral and anti-chiral microstructures belong to this class and their design and optimization requires a deep knowledge of their mechanical behaviour.

Identification, Analysis and Control of Dynamical Systems

The course provides an introduction to dynamical systems, with emphasis on linear systems. After introducing the basic concepts of stability, controllability and observability, the course covers the main techniques for the synthesis of stabilizing controllers (state-feedback controllers and linear quadratic regulators) and of state estimators (Luenberger observer and Kalman filter). The course also covers data-driven approaches of parametric identification to obtain models of dynamical systems from a set of data, with emphasis on the analysis of the robustness of the estimated models w.r.t.


This course introduces students to the basic concepts used in quantitative finance, which forms the basis for many applications such as derivatives pricing, financial engineering and asset pricing. Anyone interested in these areas will have to acquire a good grasp of the topics in this course.