Image Analysis

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.

Advanced Topics of Image Analysis

This course will be organized as series of reading groups or specialized seminars by members or collaborators of the research unit on Pattern Recognition and Image Analysis (PRiAn).

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.

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.

Software Engineering for Service-Oriented Systems and Autonomic Systems

Service-Oriented Computing is an emerging paradigm where services are understood as autonomous, platform-independent computational entities that can be described, published, categorised, discovered, and dynamically assembled for developing massively distributed, interoperable, evolvable systems and applications. In this course a model-driven approach to the development of service-oriented software systems is presented where foundational theories and techniques are integrated in a pragmatic software engineering approach.

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.

Advanced Topics of Computer Science

This course will be organized as series of reading groups or specialized seminars by members or collaborators of the research unit on System Modelling and Analisys (SysMA).

Large Scale Image Analysis for Natural and Life Sciences

Principles of imaging modalities (optical microscopy, spectroscopy, CT, MRI, PET, SPECT) and their applications in natural and life sciences (Dharmakumar); Basics of image analysis (filtering, segmentation, detection) and basics of statistical mining; Designing robust image analysis methods; Large-scale analysis; Integration with databases and knowledge sharing platforms; Error testing and precision bound repetition studies for longitudonal and group studies (phenotyping); High performance computing for imaging (computer vision); Scientific and data visualization; Prerequisites: Probability an

Convex Optimization

The course aims at giving a modern and thorough treatment of algorithms for solving convex, large-scale and nonsmooth optimization problems. Applications of convex optimization. Convex sets, functions and optimization problems. Optimality conditions. Basic algorithms for unconstrained optimization (gradient, fast gradient and Newton methods). Basic algorithms for constrained optimization (Interior point and active set methods). Subdifferential and conjugate of convex functions. Duality. Proximal mappings. Proximal minimization algorithm. Augmented Lagrangian Method.