Sign In


Sort by AttachmentsUse SHIFT+ENTER to open the menu (new window).
Theory and Application of Timed Automata Model CheckingUse SHIFT+ENTER to open the menu (new window).
Prof. Frits Vaandrager, Radboud University Nijmegen
Motivation/Overview: As our daily lives depend increasingly on digital systems, the reliability of these systems becomes a concern of overwhelming importance, and as the complexity of the systems grows, their reliability can no longer be sufficiently
controlled by traditional approaches of testing and simulation. It becomes essential to build mathematical models of these systems, and to use (algorithmic) verification methods to analyse these models. During recent years there has been enormous
progress in the area of model checking. In this course, an overview will be presented of model checking tools&techniques for timed automata, a framework that is particularly useful for the specification and analysis of embedded systems. The
application of these techniques will be illustrated on industrial sized examples taken from the areas of embedded real-time systems, distributed algorithms and protocols.
Participants learn how to make models and how to analyse them using state-of-the-art techniques and tools.
Objectives: After successful completion of the
course, participants are able to:
  • recognize situations in which the applications of timed automata model checking
    techniques for specification and analysis may be useful,
  • explain the modelling framework and basic theory of timed automata,
  • model (critical parts of) embedded systems as networks of timed automata,
  • formalize desired properties of these systems in terms of automata or temporal logic,

Period: 2-14 May

May 2:       9 - 12

May 3-6:    9 - 11

May 9-11:   9 - 11

Proof theory with applications to computation and deductionUse SHIFT+ENTER to open the menu (new window).
Prof. Dale Miller, Ècole Polytechnique, LIX
The first week (the first 10 hours) will cover material taken from my lecture notes titled "Proof Search and Computation" (draft dated February 2010 or later). The goals of this first week are
  1. introduce the students to the basics of the sequent calculus,
  2. provide some formal results covering the proof-search approach to computation,
  3. present the basics of linear logic and how it can be used to make the logic
    programming paradigm more expressive.

The second week (the second 10 hours) will expand the role of the sequent calculus from the specification of logic programming computations to the more general settings of model checking and induction.

Period: 12-24 September  --  daily 9-11 -- Sala Riunioni Ovest

Ambient Intelligence, Media, and SensingUse SHIFT+ENTER to open the menu (new window).
Nicu Sebe, University of Trento

I. Synopsis
This course will focus on three main areas:
(1) multimodal interaction: visual (body, gaze, gesture) and audio (emotion) analysis;
(2) image databases, indexing, and retrieval: context modeling, cultural issues, and machine learning for user-centric approaches;
(3) multimedia data: conceptual analysis at different levels (feature, cognitive, and affective).

II. Motivation
Computer Vision plays a fundamental role in many new types of interfaces and application areas (multimodal and attentive interfaces, applications such as surveillance, medicine, art, etc.) in which humans play a central role. This implies that building Computer Vision systems (e.g., for human-computer interaction, etc.) lies at the crossroads of many research areas (psychology, artificial intelligence, pattern recognition, multimedia, etc.). Although many existing intelligent systems were designed with human uses in mind, many of them are far from being user friendly or are rooted on real-world human-needs (few Computer Vision systems can be considered "Human-Centered"). What are the current trends in computing and what can the scientific/engineering community do to effect a change for the better?

On one hand, the fact that computers are quickly becoming integrated into everyday objects (ubiquitous and pervasive computing) implies that effective natural humancomputer
interaction is becoming critical (in many applications, users need to be able to interact naturally with computers the way face-to-face human-human interaction takes place). On the other hand, the wide range of applications that use multimedia, and the amount of multimedia content currently available, imply that building successful computer vision and multimedia applications requires a deep understanding of multimedia content. The success of human-centered vision systems, therefore, depends highly on two joint aspects:

  1. the way humans interact naturally with such systems (using speech and body language) to express emotion, mood, attitude, and attention, and
  2. the human factors that pertain to multimedia data (human subjectivity, levels of interpretation).

This course takes a holistic approach toward developing human-centered vision systems. The aim is to identify the important research issues, and to ascertain potentially fruitful future research directions in relation to the two aspects above. In
particular, the course will introduce key concepts, discuss technical approaches, and open issues in three areas:

  1. multimodal interaction: visual (body, gaze, gesture) and audio (emotion) analysis;
  2. image databases, indexing, and retrieval: context modeling, cultural issues, and
    machine learning for user-centric approaches;
  3. multimedia data: conceptual analysis at different levels (feature, cognitive, and affective).

The focus of the course, therefore, is on technical analysis and interaction techniques formulated from the perspective of key human factors in a user-centered approach to developing Human-Centered Vision Systems.

III. Benefits & List of Topics
This course will enable the understanding of key concepts, state-of-the-art techniques, and open issues in:

  • Media sensing and processing, sensor data management, mining, and data streams, basic signal processing
  • Vision for multimodal interaction: overview of techniques and state of the art in
    body tracking, gaze detection, and gesture recognition.
  • Multimodal emotion recognition for affective retrieval and in affective interfaces: approaches to multimedia content analysis and interaction that use speech and facial
    expression recognition.
  • Machine learning: adaptive multimodal interfaces and learning of visual concepts from user input for automatic detection and recognition (detection of scenes, objects,
    or events of interest).
  • Multimodal fusion: technical approaches and issues in combining multiple media (e.g., audio-visual) for multimodal interaction and multimedia analysis.
  • Multimedia indexing: an overview of how humans perceive, index, organize, and search multimedia content. Discussion of studies in art, psychology, library sciences,
    and the development of conceptual frameworks for computational frameworks.
  • Human issues: the role of memory, subjectivity, culture, context, and examples of technical approaches to multimedia analysis and interaction that consider these
  • Applications: traditional and emerging application areas will be described with specific examples in smart conference room research, arts, interaction for people with
    disabilities, entertainment, and others.

IV. Materials
This course will be specifically designed for a broad audience -- while the focus of the course will be technical, the aim is to give the students a broad view of research and important topics for developing Human-Centered Vision Systems. Materials will
include overviews of technical approaches for Vision-Based Human-Computer Interaction, Human-centered Computing, Artificial intelligence, etc.


Period: 16 May      ---     16.30 -- 18.30 Sala Seminari Ovest

            17-20 May and 30 May - 3 June      ---     10 -- 12 Sala Seminari Ovest

Structured parallel programmingUse SHIFT+ENTER to open the menu (new window).
Marco Danelutto
Da definire
From Mobility Data Management to Privacy-aware Analysis and Locationbased ServicesUse SHIFT+ENTER to open the menu (new window).
Yannis Theodoridis, Nikos Pelekis (U. Piraeus)

A flood of data pertinent to moving objects is available today, and will be more in the near future, particularly due to the automated collection of telecom data from mobile phones and other location-aware devices. Such wealth of data, referenced both in space and time, may enable novel classes of applications and services of high societal and economic impact, provided that the discovery of consumable and concise knowledge out of these raw data is made possible. Recent research activities have developed theory, techniques and systems for geographic (particularly, mobility) data management and analysis as well as services that take advance of this data, the socalled Location-based Services (LBS).

In this course, we will present the required infrastructure, Moving Object Database (MOD) engines, as well as methods and
techniques for efficient management, analysis, and mining of mobility data, towards advanced location-aware applications and services. The theoretical lectures will be accompanied and synchronised with exercises and hands-on experience lab modules on a robust and widely cited MOD engine.

Course Outline (proposed: 15 hrs theory + 5 hrs labs)

  • Introduction
  • the background (2 + 0 hrs): GIS and Spatial DBMS; An overview of LBS
  • Mobility database management (3 + 3 hrs): Models and systems for MODs; MOD indexing and querying
  • Mobility data analysis (3 + 2 hrs): OLAP and KDD techniques for MODs
  • Location-based services (2 + 0 hrs): Location- vs. trajectory- aware LBS
  • Privacy aspects on mobility data management (3 + 0 hrs): Privacy-preserving LBS and KDD
  • Outlook (2 + 0 hrs): Open research issues; project proposals
Geospatial Visual AnalyticsUse SHIFT+ENTER to open the menu (new window).
Gennady and Natalia Andrienko, Fraunhofer FIAIS, Bonn, Germany

The course introduces Visual Analytics – a new research discipline defined as the science of analytical reasoning facilitated by interactive visual interfaces. Visual analytics combines automated analysis techniques with interactive visualizations so that to extend the perceptual and cognitive abilities of humans and enable them to extract useful information and derive knowledge from large and complex data and to solve complex problems. Particularly, data and problems involving geospatial components and time are inherently complex and therefore call for visual analytics approaches.
We present a system of exploratory data analysis tools and methods, including interactive maps, statistical graphics and multiple coordinated displays, data transformations applicable to spatial and temporal data, and appropriate computational techniques such as cluster analysis and aggregation. We consider analytical questions related to spatial time series and to spatially
distributed events, describe general types of patterns that can be found in such data, and suggest appropriate visual analytics methods.

We discuss in more detail the problems of analyzing data about movement of various discrete objects in geographical space. We consider three types of movement data: data describing movements of a single entity during a long time period, data
about simultaneous movements of multiple unrelated entities, and data about simultaneous movements of multiple related entities. The pertinent analysis tasks significantly differ for these types of data. For each type of data, we briefly introduce the visual analytics techniques and tools we have developed in the recent years.

Correctness by Construction with SPARKUse SHIFT+ENTER to open the menu (new window).
Carlo Montangero

Preliminary program:
Language issues: restrictions for verification feasibility.
Verification I: information flow control.
Verification II: design by contract.
Verification III: data abstraction and refinement.
Tool support


The purpose of the course is to present state-of-the-art techniques and tools to develop secure, safe, and modular programs. SPARK is a real language - a sub/superset of Ada - and an environment that supports automatic verification to large extent. Verification is based on the classical pre-post conditions approach. The course will provide adequate introduction to the tools.
Language issues: restrictions for verification feasibility.
Verification I: information flow control. Tool support.
Verification II: design by contract. Tool support.
Verification III: data abstraction and refinement. Tool support.
J. Barnes. High Integrity Software. Addison Wesley. 2006. ISBN 978-0-321-13616-9.

Assessment: either a project in SPARK or a seminar on competitive techniques.


First lecture June 16, 2011 -- Aula seminari est
Calendar (tentative):
Following lectures (modulo other agreements): Tuesday-Thursday 11-13, same room.

Resiliency in cloud e overlayUse SHIFT+ENTER to open the menu (new window).
F.Baiardi, L.Ricci, D.Sgandurra

Il corso è focalizzato sulle metodologie che permettono di aumentare sicurezza ed affidabilità in reti virtuali complesse quali quelle che sono alla base delle strategie utilizzate da sistemi cloud o P2P. In questa ottica vengono presentate tecnologie di virtualizzazione, meccanismi e politiche per affrontare e risolvere i nuovi problemi di sicurezza ed affidabilità posti da questi sistemi. Infine sono discusse le metodologie e gli algoritmi per la diffusione affidabile di informazioni su reti virtuali.

The course is focused on the methodologies that aims to improve security and safety in complex virtual networks such as those underlying cloud or p2p computing. In perspective, we will present virtualization technology as an enabling technology, policies and mechanisms to solve the challenging security problems posed by cloud computing and a set of algorithms to improve the safety of p2p system together with the mathematical model to evaluate the advantages of their adoption


F.Baiardi (FB)

L.Ricci,  (LR)

D.Sgandurra, (DS)


Sistemi Cloud: definizioni di base, proprietà e tecnologie abilitanti       2 ore    FB        

Modello dei guasti e delle minacce     2 ore    FB

Attacchi e contromisure

    cloud cartography                           2 ore    FB

    proof of retrievability                       2 ore    FB

    xss e xsrf                                        2 ore    FB

    introspezione, attestazione             2 ore    DS

    homomorphic encryption                2 ore    FB

Epidemic Protocols

                   algoritmi di gossip: peer sampling, security                  2  ore       LR              

    modelli matematici per algoritmi epidemici            2 ore     LR

                   applicazioni                                              2 ore     LR


Cloud Computer: Taxonomy and Enabling Technologies        2 h.    FB        

Threat Modelling                                                                      2 h.    FB

Attacks and Countermeasures

    cloud cartography                         2 h.    FB

    proof of retrievability                     2 h.    FB

    xss /xsrf                                        2 h.    FB

    introspection, attestation, trusted computing        2 h.    DS

    homomorphic encryption                                      2 h.    FB

Epidemic Protocols

                   gossip algorithms: peer sampling, security           2 h.     LR              

    mathematical models for epdemic algorithmi                       2 h.     LR

                   applicazioni                                                            2 h.     LR

Periodo:     Settembre/Ottobre 2011

Esame:     seminario su argomenti presentati nel corso

High Performance Computing and Enabling Platforms, 6 CFU, in inglese, primo semestreUse SHIFT+ENTER to open the menu (new window).
Marco Vanneschi
Abstract: This course deals with two strictly interrelated issues:
1. fundamental concepts and techniques in parallel computation structuring and
design, including parallelization methodologies and paradigms, parallel programming
models and their implementation, and related cost models;
2. architectures of high-performance computing systems, including shared memory
multiprocessors, distributed memory multicomputers, clusters, and others.
Both issues are studied in terms of structural models, static and dynamic support to
computation and programming models, performance evaluation, capability for
building complex and heterogeneous applications and/or enabling platforms, also
through examples of application cases. Technological features and trends are studied,
in particular multi-/many-core technology and high-performance networks
Distributed Systems: Paradigms and ModelsUse SHIFT+ENTER to open the menu (new window).
Marco Danelutto
9 CFU, nel secondo semestre
Apprendimento Automatico: Reti Neurali e Metodi AvanzatiUse SHIFT+ENTER to open the menu (new window).
Alessio Micheli
Crediti: 6, Semestre: 2
È un corso avanzato di Machine Learning, per il design di modelli innovativi e
metodologico per applicazioni in aree interdisciplinari
Elaborazione del Linguaggio NaturaleUse SHIFT+ENTER to open the menu (new window).
Giuseppe Attardi
secondo semestre
Reti Mobili: Reti ad hoc e di sensori Use SHIFT+ENTER to open the menu (new window).
Stefano Chessa
II semestre
STT - Semantica e Teoria dei TipiUse SHIFT+ENTER to open the menu (new window).
Ugo Montanari
Modelli di Calcolo di Sistemi Funzionali, Concorrenti e Interattivi
Finalita' del Corso
Verranno presentate alcune proprietà
fondamentali dei modelli di calcolo, come la
semantica operazionale ed astratta, la struttura
dei tipi, l'ordine superiore, la concorrenza,
l'interazione. Verranno utilizzate la semantica
algebrica e la teoria elementare dei tipi, ma
non vi sono prerequisiti eccetto una conoscenza
elementare dell'algebra e della logica.

Programma del Corso
Il lambda calcolo con tipi semplici
L'isomorfismo di Curry-Howard
Il PCF e il suo modello cpo, con applicazione ai
linguaggi di programmazione funzionali
Elementi di tipi ricorsivi e polimorfi, con
applicazione ai linguaggi di programmazione
orientati agli oggetti
Le categorie come algebre parziali
Categorie monoidali, cartesiane e cartesiane chiuse (CCC)
Le CCC come modelli del lambda calcolo con tipi semplici
Specifiche algebriche, categorie di modelli e aggiunzioni
La semantica operazionale come costruzione universale
Le reti di Petri e i loro modelli monoidali (strettamente) simmetrici
I sistemi di riscrittura etichettati (LTS) come coalgebre
I sistemi LTS composizionali come bialgebre
Il Calculus for Communicating Processes (CCS) e
il Pi-calcolo di Milner e i loro modelli

Materiali Didattico:
John Mitchell, "Foundations for Programming
Languages", MIT Press, 1996. Capitoli:
Note manoscritte.

Orario del Corso
mercoledi' 11.00-13.00 in Aula Mancini
venerdi' 11.00-13.00 in Aula Mancini.

Modalita' d'Esame
Da definire.