Phd courses of previous academic years - Area Dottorato

a.y. 2020/2021

Rigorous Modelling Methods for Software Engineering

Lecturer: Egon Boerger

The course introduces a rigorous method to model software-intensive systems at different levels of abstraction which can be related by provably correct refinement statements that faithfully link application domain to programmers’system views. The used technical concept is that of Abstract State Machines, a form of pseudo-code which extends finite state machines to programs working on abstract data types at any level of abstraction and can be given a simple precise semantics. The method is illustrated by modeling real-life case studies in various domains: control systems, Java/C# program interpreter, thread handling, programming patterns, process networks (distributed network algorithms, routing protocols in mobile ad hoc networks (AODV), weak shared memory db management (Cassandra)), business processes (WebServiceProvider, SardexBusinessLogic), concurrent systems. Participants will be invited (and supported) to try out their own models for concepts they are working on.

Foundation of Computing

Lecturers: Ugo Montanari

(Note that this course is open to Ph.D students but it is actually a MS course. It therefore consists of aroung 48 hours of classes spread from mid February till mid of May, with only 4 hours of classes per week.)

Students learn the essential properties of some widely employed models of computation for higher order, concurrency, interaction, mobility. Algebraic semantics and elementary category theory are employed.

Basic Principles of Security and Blockchain

Lecturers: Laura Ricci, Fabrizio Baiardi

Blockchain technology has a great potential to radically change our socio-economical systems by guaranteeing secure transactions between untrusted entities, reducing their cost and simplifying many processes. Such a technology is going to be exploited in many different areas like IoT, social networking, health care, electronic voting and so on. Even if several applications are already leveraging its disruptive potentials, the basic principles of this technology deserve further research. Furthermore, this technology is strictly related to the general theme of the security of information system. For this reason, the course will present, in the first part, some basic concepts of information system security, then it will discuss the basic pillars of blockchains, like consensus and game theory. The first 6 hours will deal with Security issues: ICT Risk Assessment, Adversary Simulation, MITRE Attack Matrix, Offensive Security and Attack Platform, ICT Resilience. The other 10 hours will deal with Blockchain issues: Fault Tolerance & Paxos, Distributed Consensus: basic definitions, Byzantine Agreement, Eventual Consistency, Game Theory, Distributed storage, Blockchain: consensus models.

Design Thinking for Scientists

Lecturers: Daniele Mazzei

Design Thinking is an iterative process in which we seek to understand the user, challenge assumptions, and redefine problems in an attempt to identify alternative strategies and solutions that might not be instantly apparent with our initial level of understanding. Design Thinking provides a solution-based approach to solving problems. It is a way of thinking and working as well as a collection of hands-on methods. Design Thinking is not an exclusive property of designers all great innovators in literature, art, music, science, engineering, and business have practiced it. The course will introduce to design thingin and human centered design approaches giving PhD students an overall view on how this methods can be applied to the research context.

Reinforcement Learning

Lecturers: Davide Bacciu

The course will introduce students to the fundamentals of reinforcement learning (RL). We will start by introducing RL problem formulation, its core challenges and a survey of consolidated approaches from literature, including dynamic programming, value-function learning and policy learning. We will then cover model-based RL and exploration strategies. Finally, the course will discuss more recent reinforcement learning models that combine RL with deep learning techniques.

A student successfully completing the course should be able to lay down the key aspects differentiating RL from other machine learning approaches. Given an application, the student should be able to determine (i) if it can be adequately formulated as a RL problem; (ii) be able to formalise it as such and (iii) identify a set of techniques best suited to solve the task, together with the software tools to implement the solution.

Program analysis for verification

Lecturers: Letterio Galletta (IMT), Pierpaolo Degano

This course provides an overview of advanced techniques for analyzing software and for checking their properties. The lectures will present the theory underlying various techniques as well as demonstrations of software tools that implement them. Moreover, the lecture will illustrate how advanced static analysis techniques are applied in the field of computer security, Internet of Things, smart contract and safe AI. The course will mix theory and practice; students will formalize analyses and prove them correct, will implement analyzers from scratch, and also will experience state of the art static analysis tools.

Programming Tools and Techniques in the Pervasive Parallelism Era

Lecturers: Marco Danelutto, Patrizio Dazzi (CNR ISTI)

The course covers techniques and tools (already existing or that are in the process of being moved to mainstream) suitable to support the implementation of efficient parallel/distributed applications targeting small scale parallel systems as well as larger scale parallel and distributed systems, possibly equipped with different kind of accelerators. The course follows a methodological approach to provide a homogeneous overview of classical tools and techniques as well as of new tools and techniques specifically developed for new, emerging architectures and applicative domains. Perspectives in the direction of reconfigurable coprocessors and domain-specific architectures will also be covered.

Quantum Computing

Lecturers: Fabrizio Luccio, Simone Montangero (UNIPD), Patrizia Gianni, Roberto Bruni, Fabio Gadducci

Nine lectures of two hours each, presented by scholars of different disciplines and directed mainly to Ph.D. students of Computer Science. Fabrizio Luccio introduce the whole course, with a computer scientist’s overview of quantum computing. Then a set of lectures will be given by Simone Montangero on the principles of quantum mechanics and their applications in quantum computation and information. Patrizia Gianni will present Shor’s and Grover’s quantum algorithms and their extensions. Finally, Roberto Bruni and Fabio Gadducci will discuss Quantum programming languages.

Final evaluation of the participants: Study and written presentation of scientific material, to be agreed with one of the lecturers.

Algorithmic Tools for Massive Network Analytics

Lecturers: Roberto Grossi, Paolo Boldi (UNIMI), Alessio Conte, Andrea Marino (UNIFI), Giuseppe Italiano (LUISS), Giordano Da Lozzo (Roma Tre), Fabio Vandin (UNIPD)

Many complex real-world phenomena are naturally modeled as networks: social interactions, internet/web, knowledge bases, power grids, financial transactions, biological pathways, to name a few. Network analysis aims at finding interesting properties hidden in the linked structure. This analysis is challenging from a computational point of view due to the sheer size of the networks and the combinatorial nature of the corresponding graph problems. These lectures will present some powerful combinatorial algorithms for graphs and provide an algorithmic toolkit to store, analyze and extract meaningful patterns from large-scale networks.

Monte Carlo methods and sampling for computing

Lecturers: Francesco Banterle (CNR)

This course introduces students to Monte Carlo methods and sampling techniques with a focus on visual computing. These are crucial to accelerating the computations of a variety of computational simulations where we need to draw high-quality samples or to integrate a complex multi-dimensional function such as physically-based rendering for computing the radiance of buildings, estimating the price of options, or how epidemics spread out. At the end of this course, students will have both theoretical and practical tools that they can apply to a variety of problems to achieve high-quality solutions. During the course, students will see and study successful examples of this beautiful theory to visual computing; e.g., visual processing, computational finance and biology.

Algorithmic Game Theory

Lecturers: Giancarlo Bigi

The lectures aims at introducing the main paradigms of game theory within an algorithmic perspective in order to analyse the behaviour of multi-agent systems and phenomena. Suitable mathematical models and tools will be provided to help the understanding of inner mechanisms of competition and cooperation, threads and promises. A few application to problems from different areas are provided upon the students’ interests (for instance, computational economics, traffic and social networks, security, distributed computing and machine learning). A critical analysis of the power and limitations of game theory is addressed as well.

a.y. 2019/2020

Cyber-Physical Systems and Cloud for Smart Industry

Lecturers: Daniele Mazzei (UNIPI)

IOT, Industrial IOT, sensors and edge gateway are disruptively changing our factories connecting machines, people and apparatus to cloud architectures aimed at supporting the management in the improvement of production efficiency. The course will explore different Industrial technologies highlighting the architectural paradigms and strategy used for the design, development, deploy and maintenance of smart factory.

Design-by-Contract and Behavioral Types

Lecturers: Roberto Bruni (UNIPI), Hernan Melgratti (University of Buenos Aires)

The design-by-contract approach promotes the usage of executable specifications to describe the mutual obligations that regulate the interaction between different modules. Contracts are embedded in code and checked at runtime to help developers identify faulty modules. Behavioral types instead provide a description of the interaction aspects of a program and are used to specify the communication protocols that regulate the communication among distributed components. In this course we will present the current approaches for combining contracts and behavioral types. We will cover the following topics: Design-by-Contract approach (DbC), Higher-order contracts (Findler & Felleisen), Binary Session Types, Chaperone contracts for session types, Multiparty Session Types (MST), DbC for MST, Dependent Session Types.

Theory of Computing

Lecturer: Ugo Montanari (UNIPI)

Some basic properties of models of computation are studied, like operational and abstract semantics, typing, higher order, concurrency, interaction. Algebraic semantics and elementary category theory are employed, but no prerequisites are required except for some elementary knowledge of logic and algebra.

Shape Analysis and Geometry Processing

Lecturers: Paolo Cignoni (CNR ISTI), Fabio Ganovelli (CNR ISTI), et alii

The course deals with 3D shape analysis and geometric processing, which are key topics in Computer Graphics, Vision and Digital Fabrication. The course introduces well established and recent geometric concepts and tools (curvature and geodesics, spectral methods, computational topology, topological persistence), emphasizing the discrete and computational viewpoint. In the last decades these topics have attracted the attention of many researchers thanks to the fast-paced growth of the research in 3D, pushed by the technological advances in gaming, autonomous navigation, biomedical, digital cultural heritage, 3D printing, etc. The aim of the course is to let the math student appreciate how geometry is successfully used in applied sciences; and to provide the computer science student the mathematical basis needed to efficiently tackle open issues in such a lively research field.Computer Science PhD students are suggested to take the module of 16h concerning more on the algorithmic aspects, just talk to the lecturers.

Reinforcement Learning

Lecturer: Davide Bacciu (UNIPI)

The course will introduce students to the fundamentals of reinforcement learning (RL). The course will start by recalling the machine learning and statistics fundamentals needed to fully understand the specifics of RL. Then, it will introduce RL problem formulation, its core challenges and a survey of consolidated approaches from literature. Finally, the course will cover more recent reinforcement learning models that combine RL with deep learning techniques.

Space will be devoted to present RL applications in areas that are relevant for students of industrial and information engineering, such as robotics, pattern recognition, life sciences, material sciences, signal processing, computer vision and natural language processing. The course will leverage a combination of theoretical and applicative lectures.

Programming Tools and Techniques in the Pervasive Parallelism Era

Lecturers: Marco Danelutto (UNIPI), Patrizio Dazzi (CNR ISTI)

a.y. 2018/2019

Matrix computations: a quick overview and some applications

Lecturer: Gianna Del Corso (UniPI), Federico Poloni (UniPI)

We overview some useful techniques of numerical linear algebra with several applications to data analysis. The theoretical aspects will be complemented with a few examples from applications. Theory: review of singular value decomposition and other factorizations, Kronecker products, Fast Fourier transform, nonnegative matrix factorizations, nonnegative matrices and M-matrices. Applications: image deblurring / denoising, vector space model, latent semantic indexing, clustering, Pagerank / invariant measures of Markov chains, Centrality measures.

Genomic data analysis with applications

Lecturer: Ugo Borello (Biologia, UniPI), Filippo Geraci (IIT CNR)

The goal of the course is to introduce the main framework for computational analysis of genomic data: from differential analysis to integration of omics data and biological networks.

We focus on data generated by Next Generation Sequencing (NGS) technology and we discuss the impact of these technologies on biology and bioinformatics.

NGS data analysis is the first step to differential analysis, which is the task of measuring a certain (often large) number of variables in two different populations of biological samples and deriving the subset of variables that are statistically different. We will see several techniques and applications of differential analysis: from differential expression to the discovery of biomarkers. To this end, we will also review the basics of clustering, classification and feature selection.

Subsequently, we will introduce the problem of multi-omics data analysis, its advantages and challenges. We will focus on the integration of data coming from different technologies reviewing different state-of-the-art methods.

In the last part of the course, we will introduce the network structure of biological data. We will show how some problems in graph theory are closely related to biological problems. For example, we will see how the problem of finding protein complexes can be easily mapped into the problem of finding communities in a graph.

Polyhedral Combinatorics

Lecturer: Laura Galli (UniPI), Adam Letchford (University of Lancaster, UK)

Many important optimization problems arising in practical applications are discrete or combinatorial. Indeed, such problems arise in fields as diverse as operational research, statistics, computer science, engineering and the physical sciences. Although most combinatorial problems are theoretically intractable (“NP-hard”), algorithms and software have improved dramatically during the past couple of decades, to the point where real-life instances with thousands of variables and constraints can now be solved to proven optimality or near-optimality. One of the key components of this success is the study of certain convex polyhedra. The study of such polyhedra is known as polyhedral combinatorics. This course gives an introduction to this fascinating topic, covering theory, algorithms, applications and software. Topics covered: – Recap on Combinatorial Optimisation – Modelling Problems as Integer Programs – Classical Solution Approaches – Fundamentals of the Polyhedral Approach – Some Simple Polyhedra – Polyhedra Associated with NP-Hard Problems – Algorithms and Implementation – Applications

Data Stream Processing from the Parallelism Perspective

Lecturer: Gabriele Mencagli (UniPI), Matteo Andreozzi, ARM

An ever-growing number of devices are capable of sensing the world by producing huge flows (data streams) of information regarding the users and the environment. A large set of applications need efficient processing techniques to extract insights and complex knowledge from such a massive and transient data deluge. Furthermore, to keep the processing in real-time, existing systems must expose parallel features to adapt the algorithms and the way the processing is performed to unpredictable and time-varying input rates and workloads.

The computing paradigm enabling the processing in those scenarios is called Data Stream Processing, which comprises in its most general meaning other closely-related paradigms like Event Processing and Complex Event Processing. The course aims at giving a solid background on this research field, with an introduction on the theory behind stream processing, an overview of the most famous Stream Processing Systems (e.g., Apache Storm, Apache Flink and Spark Streaming) and the most recent results achieved by the scientific community in terms of optimizations, cost models and patterns. Furthermore, in the final part of the course, the FastFlow and WindFlow parallel libraries will be described in details, by outline the research advancements for ultra-low latency streaming systems targeting multi-core environments and C++ programming.

Theory and Practice of Learning From Data

Lecturer: Luca Oneto (UniPI)

This course aims at providing an introductory and unifying view of information extraction and model building from data, as addressed by many research fields like Data Mining, Statistics, Computational Intelligence, Machine Learning, and Pattern Recognition. The course will present an overview of the theoretical background of learning from data, including the most used algorithms in the field, as well as practical applications in industrial areas such as transportation, manufacturing, etc.

a.y. 2017/2018

An introduction to Deep Learning

Lecturer: Antonio Gullì (Google)

The goal of this course is to provide an handson introduction to Deep Learning. The traditional concepts used in neural networks are introduced, together with modern convolutional networks, generative adversarial networks, recurrent networks, and autoencoders. In addition, we will look at Reinforcement Learning and its application to AI Game Playing, a popular direction of research and application of neural networks. All the examples will be coded in Keras a python high-level framework running on the top of Google’s Tensorflow, Microsoft’s CNTK, Amazon’s MLXnet, and University of Montreal’s theano.

Graph Mining Algorithms

Lecturer: Andrea Marino (UniPI)

In this course we will focus on the computation of several graph topological measures, for which polynomial-time algorithms are available and in “practice” are not useful, due to the huge size of the networks to be analysed. We will consider efficient algorithms for the following problems: computing diameter, distance distribution, average distance, and centrality measures, counting triangles and probabilistic counting in general, clustering and graph pattern mining.

Shape Analysis and Geometric Processing

Lecturer: Paolo Cignoni, Fabio Ganovelli, Daniela Giorgi, Maria Antonietta Pascali (ISTI – CNR)

The course deals with 3D shape analysis and geometric processing, which are key topics in Computer Graphics, Vision and Digital Fabrication. The course introduces well-established and recent geometric concepts and tools (curvature and geodesics, spectral methods, computational topology, topological persistence), emphasizing the discrete and computational viewpoint. In the last decades these topics have attracted the attention of many researchers thanks to the fast-paced growth of the research in 3D, pushed by the technological advances in gaming, autonomous navigation, biomedical, digital cultural heritage, 3D printing, etc. The aim of the course is to let the math student appreciate how geometry is successfully used in applied sciences; and to provide the computer science student the mathematical basis needed to efficiently tackle open issues in such a lively research field.

Skills Boosting for New (Research) Horizons

Lecturer: Paolo Ferragina (UniPI), Michele Padrone (UniPI), Davide Morelli (BioBeats), Flavio Tosi (Business Exploration),Camilla Van den Boom (Eindhoven University), Nicola Redi (Venture Factory), Ray Garcia (Buyont Capital, NY)

This course aims to help PhDs in Computer Science to scale and enrich their technical and scientific abilities with experiences, (soft) skills and networking useful for your future either as a researcher, or as an entrepreneur, or as a chief software engineer, or as the CTO of a successful company ! It is indeed very well known that the best talents are found at the intersection of community/networking, skills, right mindset (good attitude and self-motivated) and technical competency. The course is intended to have PhD students to ACT on their own and be able to evaluate their scientific achievements from other perspectives, find new avenues for grant funds for research and developing their ideas.

Formal Methods for Program Verification

Lecturer: Massimo Bartoletti (UniCa), Pierpaolo Degano (UniPI), Dino Di Stefano (Facebook), Gianluigi Ferrari (UniPI), Letterio Galletta (UniPi)

We will focus on a repertoire of formal techniques that prevent applications and systems to misbehave.
This issue is particularly relevant because now-a-days software is everywhere. Thus it has to be designed to properly work in open, highly mutable environments of different nature, including cyber-physical ones.Software must then come with guarantees on its behaviour, robustness, reliablity, security, scalability, and efficiency. Precise guarantees can only be offered by a formal proof of software correctness, carried on a sound abstract model of the system in hand. We will also present and possibly experiment with mechanical tools, used in industries and academia, which support program verification.

Distributed Systems Security

Lecturer: Roberto di Pietro (College of Science and Engineering, Dhoa-Quatar)

This course focuses on fundamental and advanced concepts in Distributed Systems, addressing their foundations, current technologies, and security aspects. Topics include, but are not limited to, distributed hash tables (peer-to-peer systems), failure detectors, synchronization, election, distributed agreement, consensus, gossiping, replication, key-value stores, NoSQL, blockchain technology. These topics are discussed in the context of real-life and deployed systems such as clouds and datacenters, databases, peer to peer systems, clusters, cryptocurrencies.

Modeling methods

Lecturer: Egon Boerger (UniPI)

The course explains two major methods for design and analysis of computational systems, known as ASM (Abstract State Machines) and Event-B method. The focus will be on the refinement method which permits to link abstract models (specifications) to code in a provably correct way.

a.y. 2016/2017

Introduction to Network Science

Lecturer: Prof. Janos Kertesz (Central European University, Budapest)

Syllabus: Introduction: Complex systems and complex networks. Percolation model, scale invariance. Basic notions of graph theory. Erdős-Rényi graphs, Watts Strogatz model, configuration model, network growth models. Weighted and signed networks. Motifs and modules. Error tolerance and vulnerability against intentional attacks. Spreading problems.

Categories and Quantum Informatics

Lecturer: Prof.Chris Heunen (LFCS Univeristy of Edinburgh)

The course begins by introducing the idea behind category theory and the breadth of its scope. Why would it be a good idea to abstract away from specific hard-coded set-theoretic structures, and have compositional denotational semantics, in general? Illustrations from functional programming and categorical methods in logic are given.

We then focus more specifically on monoidal categories. Specific attention is paid to the graphical calculus, which makes the topic visually apparent. The student learns to graphically manipulate algebraic objects such as monoids and Frobenius structures. This allows perfectly rigorous proofs of correctness, and shows the information flow of a protocol that is often hidden behind superfluous details.

Throughout the course, the abstract material is linked to quantum informatics. We will categorically model notions typically thought to belong to quantum theory, such as entanglement, no-cloning, teleportation, and complementarity. But it will turn out some of these notions also make perfect sense in other settings. For example, the very same categorical description of quantum teleportation also describes classical encryption with a one-time pad. We identify characteristics of classical and quantum information, aiming to equip students to choose the right tools and techniques for future problems they may encounter.

One day of Distributed Algorithms and Graph Mining

Lecturer: Pierre Fraignaud, IRIF Université Paris Diderot – Paris 7

Design and analysis of secure systems

Lecturer: Joshua Guttman, Worcester Polytechnic Institute

First part. The focus will be on the analysis, the design, and the refinement of cryptographic protocols.

Second part. The focus will be on information flow and non-interference, I want to talk about the semantics of limited information flow, both in a non quantitative and a quantitative context, explain how these can be matched with a natural model for distributed systems, and how this promotes a compositional view of secure system development and refinement. I’d also like to indicate how the same ideas may apply to software via object capability models.

Distributed Computing and Large Graph Mining

Lecturer: Pierre Fraignaud, IRIF Université Paris Diderot – Paris 7 e PierLuigi Crescenzi

Distributed computing is a field of computer science that studies distributed systems, i.e., systems in which a collection of autonomous computing entities coordinate their actions via some communication medium. The objective of the first part of this course is to introduce the main techniques of algorithm design and analysis for distributed computing, enabling the computing entities aiming at collectively solve a common task. This part of the course will focus on the main computing models, capturing different aspects of distributed computing, including network computing, asynchrony, fault-tolerance, etc. For each model, the course will present the main techniques for (deterministic and probabilistic) algorithm design, and for deriving lower bounds and impossibility results.

In the second part of the course, we will take a graph mining roundtrip, from theory to practice and back. In particular, we will focus on the computation of several graph topological measures, for which polynomial-time algorithms are available that in “practice” are not useful, due to the huge size of the networks to be analysed. Switching to “theory”, we will show that, unfortunately, for these measures no best algorithm exists (under reasonable complexity theory assumptions). This will lead us back to “practice”: we will describe heuristics that, in the case of real-world graphs, allow us to compute these measures in linear time. These results will finally motivate our return to “theory” in order to understand the reason why, in practice, these heuristics work so well.

The Internet of Everything, Everywhere: Methods and Technologies for Internetworking Land, Air and Sea

Lecturer: Stefano Basagni, Northeastern Univ. Boston

This course provides an introduction to the latest research directions on methodologies and technologies for the emerging paradigm of the Internet of Things (IoT).

In particular, we will explore networking challenges and solutions for the three main scenarios where key IoT applications are being defined and developed:

Terrestrial networks for IoT, including challenges and trends for smart cities and connected communities;
Multi-modal communications for underwater wireless networkings, and
Flying ad hoc networking: Coordinating drones and other form of mechanical birds.

a.y. 2015/2016

Sensor networks, internet of things and smart environments

Lecturer: Michele Girolami (CNR Pisa), Alexander Kocian (Dipartimento di Informatica), Stefano Chessa (Dipartimento di Informatica)

Wireless sensors: issues and requirements
Architectures and MAC protocols
Localization and routing
Synchronization
Energy harvesting and energy management
Smart environments
ZigBee and Bluetooth

Searching by Similarity on a Very Large Scale

Lecturer: Giuseppe Amato, CNR Pisa

Foundation of Metric Space Searching
- Distance Searching Problem
- Metric Distance Measures
- Similarity Queries
- Basic Partitioning Principles
- Principles of Similarity Query Execution
- Policies for avoiding Distance Computations
- Metric Space Transformations
- Priciples of Approximate Similarity Search
- Advanced issues: Statistics, Proximity, Performance Prediction, Tree quality measures
- Advanced issues: Choosing reference points
Exact Similarity Search
- Vantage Point Trees
- AESA/LAESA
- GNAT
The M-Tree Family
- The M-Tree
- Bulk-Loading Algorithm
- Multy-Way Insertion Algorithms
- The Slim Tree
- Slim-Down Algorithm
- Pivoting M-Tree
Hash Based Methods
- D-Index
- Approximate Similarity Search with M-Tree
  - Relative Error Approximation
  - Good Fraction Approximation
  - Small Chance Improvement Approximation
  - Proximity-Based Approximation
  - PAC Nearest Neighbor Searching
  - Performance tests
- Other Approximate Similarity Search Methods
- Permutation Based Methods
  - Permutation Spearman Rho
  - PP-Index
  - MI-File
- Locality Sensitive Hashing (LSH)
  - LSH based on p-stable distributions
  - LSH with Hamming Distance

Introduction to process calculi and related type systems

Lecturer: Ilaria Castellani, Rosario Pugliese

This course aims at introducing, and motivating the use of, some basic formal methods from Concurrency Theory. It is split in two parts. Firstly, some well-known process calculi, e.g. CCS and pi-calculus, are presented together with the most commonly used techniques for defining their operational and observational semantics. Then, many type systems are presented for ensuring different properties of distributed and concurrent processes, such as e.g. correctness of interaction and security.

Coalgebre, automi e linguaggi nominali ecc

Lecturer: Bartek Klin

Structural Operational Semantics (SOS) is a simple but powerful formalism for defining transition systems of various kinds, and operations on them. SOS specifications are usually presented as families of inference rules. This presentation is simple and intuitive, but a bit ad-hoc and difficult to generalize. Bialgebras and distributive laws are more abstract and more mathematical notion of well-behaved SOS specification, based on coalgebra as an abstract theory of transition systems.

I will present the basics of the bialgebraic approach to SOS, and a coalgebraic approach to modal logics that can be used to define properties of transition systems. I will then show how to combine both approaches to derive logical distributive laws, a general theory of logical compositionality on SOS-defined systems.

The course will use some basic notions of category theory: categories, functors, natural transformations, and a little bit of monads. I will introduce these notions as needed.

The plan of the course is as follows:

– Classical SOS theory: labeled transition systems, bisimulations, Hennessy-Milner logic, SOS rules, GSOS and other formats
– Basics of category theory and coalgebra
– Coalgebraic modal logic by dual adjunctions
– Distributive laws, bialgebras, abstract GSOS
– Logical distributive laws

Machine Learning Techniques and Selected Applications for Big Data

Lecturer: Stan Matwin (Dalhousie University, Canada)

Topics:

Intro (def, challenges, nosql etc.) 2h
Linear methods 2h
Bayesian Methods 3h
Stream Data Processing: VFDTs 2h
Vizualization: basics, examples 3h
Privacy for Big Data: data summaries (scripts, Bloom filters), ABAC approaches (Acumulo) 3h
Applications: Oceans 2h
Applications: Big Data in the Public Sector 2h
Data tagging challenges for Big Data: crowdsourcing, reCaptcha 1h

a.y. 2014/2015

Perspectives in parallel programming

Lecturer: Marco Danelutto, Dipartimento di Informatica

The course will introduce several programming environments used to implement parallel applications on modern parallel architectures. A detailed introduction of the available structured parallel programming environments will be given. Optimization problems relative to different non functional concerns (performance, power management, fault tolerance) will also be described and typical experiences in different applicative domains will be discussed. Overall, the course will give the student a good perspective on the kind of problems to be solved when tackling the efficient programming of (massively) parallel systems as well as a basic knowledge relative to state-of-the-art parallel programming frameworks.

Bayesian Machine Learning

Lecturer: Guido Sanguinetti, University of Edinburgh

This is a rough summary for the Bayesian Machine Learning course. The main reference is D. Barber’s book, Bayesian Reasoning and Machine Learning; the numbers in brackets refer to Barber’s book unless explicitly stated otherwise.

Verifiable voting systems and secure protocols: from theory to practice

Lecturer: Peter Y. A. Ryan, Université du Luxenbourg

Coinductive Methods in Computer Science (and beyond)

Lecturer: Filippo Bonchi and Damien Pous, ENS Lyon

The induction principle is ubiquitous in computer science. For instance it is used to prove properties of programs involving finite data structures, such as natural numbers, lists and trees. For reasoning about concurrent programs or infinite data structures, like streams and infinite trees, one needs a dual principle — coinduction — which is the main topic of this course.
The relevance of coinductive reasoning has been usually associated with bisimilarity, a notion of equivalence that emerged at the end of the seventies in three different fields: non-well founded set theory, modal logics and concurrency theory. In the last years, coinductive methods has been studied in more and more areas of computer science, such as automata and type theory. Perhaps unexpectedly, applications to game theory and economy have been proposed recently.
We will introduce the coinductive definition and proof principles, several techniques to enhance coinductive proofs, and some algorithms to automatize such proofs. During the course, we will encounter examples stemming from different areas, with particular focus to automata and concurrency theory. If time allows, we will also give an overview to the theory of coalgebras, which is the abstract framework encompassing all these different examples.

High Dynamic Range Imaging: theory and applications

Lecturer: Francesco Banterle, Visual Computing Laboratory, CNR Pisa

Introduction to modern Imaging – 2 hrs
Introduction to high dynamic range Imaging – 1 hr
Capturing and generating the real-world lighting 4 hrs
Tone mapping HDR images for low dynamic range displays – 4hrs
Tone mapping HDR videos for low dynamic range displays – 2hrs
Inverse Tone mapping – 2hrs
HDR content formats and compression – 2hrs
High dynamic range imaging applications – 4 hrs

Searching by Similarity on a Very Large Scale

Lecturer: Giuseppe Amato, CNR Pisa

Foundation of Metric Space Searching
- Distance Searching Problem
- Metric Distance Measures
- Similarity Queries
- Basic Partitioning Principles
- Principles of Similarity Query Execution
- Policies for avoiding Distance Computations
- Metric Space Transformations
- Priciples of Approximate Similarity Search
- Advanced issues: Statistics, Proximity, Performance Prediction, Tree quality measures
- Advanced issues: Choosing reference points
Exact Similarity Search
- Vantage Point Trees
- AESA/LAESA
- GNAT
The M-Tree Family
- The M-Tree
- Bulk-Loading Algorithm
- Multy-Way Insertion Algorithms
- The Slim Tree
- Slim-Down Algorithm
- Pivoting M-Tree
Hash Based Methods
- D-Index
- Approximate Similarity Search with M-Tree
  - Relative Error Approximation
  - Good Fraction Approximation
  - Small Chance Improvement Approximation
  - Proximity-Based Approximation
  - PAC Nearest Neighbor Searching
  - Performance tests
- Other Approximate Similarity Search Methods
- Permutation Based Methods
  - Permutation Spearman Rho
  - PP-Index
  - MI-File
- Locality Sensitive Hashing (LSH)
  - LSH based on p-stable distributions
  - LSH with Hamming Distance

Sistemi di tipi calcoli di processi e di sessione

Lecturer: Ilaria Castellani, Rosario Pugliese

Il corso mira a presentare alcune tecniche formali, basate su sistemi di tipi, per l’analisi di proprietà di sicurezza in una varieta’ di calcoli di processo e di sessione. Si comincerà con l’introduzione di alcuni sistemi di tipi per la sicurezza per il CCS ed una panoramica di diverse proprietà di sicurezza, con particolare riguardo alla noninterferenza. Si passerà quindi ad approfondire lo studio di sistemi di tipi per calcoli di processi più espressivi del CCS, come il pi-calcolo. Saranno introdotti il “sorting” di Milner e il tipaggio di input/output di Pierce e Sangiorgi, il tipaggio “comportamentale” di Kobayashi, e alcuni sistemi di tipi per la sicurezza del flusso d’informazione. Infine, saranno studiati i calcoli di sessione, che permettono ai processi di organizzare le loro comunicazioni secondo un protocollo predefinito. Saranno presentati alcuni sistemi di tipi per varianti di tali calcoli con sessioni binarie con delega, con sessioni n-arie, con sessioni n-arie con delega e sicurezza, e con sessioni con monitoraggio e adattabilità.

a.y. 2013/2014

Logic, Sets, and Graphs

Lecturer: Alberto Policriti

The main goal of the course will be to build the logical and combinatorial prerequisites to present the recent decidability result relative to the Bernays-Schoenfinkel-Ramsey (BSR) class in Set Theory. We will start from the basic notions relative to the classical decision problem in Logic and discuss the celebrated Ramsey theorem, its historical motivations, and hint at some applications. The approach will consist in a construction, from elementary notions, of the material and ideas leading to the solution of the combinatorial difficulties related to the BSR class in Set Theory. The path will explore links between Set Theory and Graph Theory. This connection will be further discussed in the final part of the course.

The proof theoretic foundation of computational logic

Lecturer: Dale Miller

I will present proof theory in the Gentzen/Girard tradition and layer on it recent results on focused proof systems. I will then make systematic use of that framework to present
(1) flexible proof systems for classical, intuitionistic, and linear logics;
(2) a foundation of a range of computational logic tools, ranging from logic programming, theorem proving, and model checking; and
(3) recent work on defining a general approach to proof certificates.

Probabilistic approaches to the protection of confidential information

Lecturer: Catuscia Palamidessi

We will present the information-theoretic approach to information flow, focussing on the cases of Shannon entropy and of Rényi min-entropy.
We will link these notions with the concept of adversary.
Then we will present a recent more general approach, based on decision theory.

In the second part of this course, we will introduce the framework of differential privacy, we will present the characterizations and properties of this notion, with emphasis on its compositionality and its independence from the prior information of the adversary.We will also highlight the relation with quantitative information flow.
We will present implementations of differential privacy, and discuss the trade-off between privacy and utility of the data.
Finally, we will present an extension of differential privacy, and its application to privacy-friendly geolocation.

Algorithms for big data

Lecturers: Paolo Ferragina and Andrea Marino

Lecture 1. Data streams and sketching: Distinct counting, Frequent Items, Probabilistic Estimators, Similarity and Min-hash sketches.

Lecture 2. Sampling: sampling in networks, markov chain sampling. Applications to estimating properties of large networks.

Lecture 3. Mining in large graphs: social network analysis, clustering, community detection, spectral techniques.

Lecture 4. Dimensionality reduction: Projections, Locality sensitive hashing, Johnson Lindenstrauss.

Lecture 5. Large-scale distributed programming frameworks: Map-reduce, Pregel and examples of computation on large graphs.

Lecture 6. Diameter computation in real-world huge graphs.

Lecture 7. Distance distribution approximation and introduction to probabilistic counting.

Lecture 8: Probabilistic counting with applications

Lecture 9. Centrality measures in complex networks.

A Framework for Exploring Biology

Lecturer: Prof. Dr. Grzegorz Rozenberg

In this series of lectures we present a framework for exploring biology which consists of:

A STATIC part which is a depository of knowledge formalized by the notion of an extended zoom structure. The integrating structure of such a depository allows one to deal with the hierarchical nature of biology.
A DYNAMIC part given by a family of reaction systems. They originated as models for processes instigated by the functioning of living cells, and they address two important aspects of biology: non-permanency of its entitities and open system aspect of biological units such as living cells.

In this setup the depository of static knowledge given by an extended zoom structure is
explored by computations/processes provided by reaction systems, where this exploration can use/integrate knowledge present on different levels (e.g., atomic, cellular, organisms,
species, …. levels).

Research topics in this framework are motivated by biological considerations as well as
by the need to understand the underlying structure of knowledge as well as the
structure of computations exploring this knowledge. The models we discuss turned out to be
novel and attractive also from the theory of computation point of view.

The lectures are of interest to mathematicians and computer scientists interested
in formal models of computation and in modelling biological processes as well as to
bioinformaticians, biochemists, and biologists interested in foundational/formal understanding of biological processes. They are of a tutorial style and self-contained. In particular, no prior knowledge of biochemistry or cell biology is required.

The presented framework was developed jointly with A. Ehrenfeucht from University of Colorado at Boulder

Computer-aided cryptography

Lecturer: Dr. Gilles Barthes

Computer-aided cryptography is an emerging approach to designing and analyzing cryptographic constructions. Its primary focus is to build machine-checked frameworks for the construction and verification of security proofs of cryptographic systems. In the form of tools like EasyCrypt, verified security has been used for verifying emblematic examples of public-key encryption schemes, digital signature schemes, hash function designs, and block cipher modes of operation. Moreover, computer-aided cryptography allows narrowing the gap between provable security and cryptographic implementations, which remains one major issue in the deployment of cryptographic systems. However, the role of computer-aided cryptography is not limited to security proofs, and there exist automated tools for discovering new cryptographic constructions, or automatically finding attacks on existing ones.

The purpose of the course is to motivate the role of computer-aided cryptography, and to give an overview of some recent developments. The main emphasis of the course will be on computer-aided cryptographic proofs, and more specifically on EasyCrypt. The course will describe the foundations of EasyCrypt, provide an introduction to provable security using EasyCrypt, and will cover some representative topics in computer-aided cryptography.

Specification methods

Lecturer: Egon Börger

Week 1: Introduction of the methods
Goal, main ingredients and characteristic uses of the methods
– Introductory examples: sluicegate, trafficlight, packagerouter, lift
Definition of:
– Logical foundation (for mono-agent models)
– Synchronous (parallel)/asynchronous (distributed) models
– CoreAsm interpreter to execute ASMs
– Rodin tool platform for Event-B

Week 2: Refinement method
Definition and Shortest Path example
– Java/JVM case study

Week 3: Modeling patterns, web services, business processes
– Programming, Workflow and Web Service Mediation patterns
– Browser/Server client/server architecture
– Business Process Modeling: BPMN vs S-BPM

a.y. 2012/2013

Security at work

Lecturer: Luca Viganò

In the Internet of Services (IoS), systems and applications are no longer the result of programming components in the traditional meaning but are built by composing services that are distributed over the network and reconfigured and consumed dynamically in a demand-driven, flexible way. However, composing services leads to new, subtle and dangerous, vulnerabilities due to interference between component services and policies, the shared communication layer, and application functionality.
I will present the AVANTSSAR Platform and the SPaCIoS Tool, two integrated toolsets for the formal specification and automated validation of trust and security of applications in the IoS at design time and run time, respectively. Both toolsets have been applied as a proof of concept on a set of security problem cases drawn from industrial and open-source IoS application scenarios, thereby paving the way to transferring project results successfully to industrial practice and to standardization bodies and open-source communities.
I will present also a number of particular results that have been obtained in the AVANTSSAR and SPaCIoS projects, such as previously unknown attacks, compositionality results, novel attacker models and techniques for efficient security verification and testing.

Iterative rounding

Lecturer: Fabrizio Grandoni

Iterative Rounding is a recent, and very powerful tool to design approximation algorithms. The basic idea is as follows. One solves a (carefully chosen) linear programming relaxation of the considered NP-hard problem. Then one rounds some variable in the fractional solution (which corresponds to fixing part of the solution under construction) according to proper rounding rules.

The problem is then simplified, and the process is iterated on the residual problem until a solution to the original problem is obtained. Alternatively or in combination to rounding, one can also relax (i.e. drop) one constraint. This leads to “slightly” infeasible solutions. In these seminars we will describe a representative sample of the most relevant results obtained via iterative rounding in the literature.

The seminars will be tentatively organized as follows. In the first week, we will introduce approximation algorithms, and present a few foundamental results and techniques in the area. The second week will be devoted to approximation algorithms based on linear programming. We will first introduce linear programming, and then present some LP-based techniques in approximation algorithms. The final part of the week will be devoted to iterative rounding.

Diffusion of information in static and dynamic graphs

Lecturer: Pierluigi Crescenzi

Rumor spreading is a well-known gossip-based distributed algorithm for disseminating information in large networks. According to the synchronous push version of this algorithm, an arbitrary source node is initially informed, and, at each time step (a.k.a., round), an informed node u chooses one of its neighbors v uniformly at random, and this node becomes informed at the next time step. In the symmetric pull version of the algorithm, at each time step, a not informed node u randomly chooses one of its neighbors v; if v is informed, then u becomes informed at the next time step.

Finally, the push-and-pull version is a combination of the two previous versions, in which, at each time step, each informed node executes a “push operation”, and each not informed node executes a “pull operation”. Rumor spreading was first introduced in the context of replicated databases, as a solution to the problem of distributing updates and driving replicas towards consistency. Successively, it has been proposed in several other application areas, such as failure detection in distributed systems, peer-sampling, adaptive machine discovery, and distributed averaging in sensor networks. Apart from its applications, rumor spreading has also been deeply analyzed from a theoretical and mathematical point of view. In particular, the completion time of rumor spreading, that is, the number of steps required in order to have all nodes informed, has been investigated in the case of several different network topologies, such as complete graphs, hypercubes, random graphs, and preferential attachment graphs. Besides obtaining bounds on the completion time of rumor spreading, most of these works also derive deep connections between the completion time itself and some classic measures of graph spectral theory, such as, for example, the conductance of a graph. The techniques and the arguments adopted in these studies strongly rely on the fact that the underlying graph is “static” and does not change over time. It is then natural to ask ourselves what is the speed of rumor spreading in the case of “dynamic” networks, where nodes and edges can appear and disappear over time (several emerging networking technologies such as ad hoc wireless, sensor, mobile networks, and peer-to-peer networks are indeed inherently dynamic). In this dynamic environment, even in the case of the simplest communication protocol that implements the broadcast operation, that is, the flooding protocol (according to which a source node is initially informed, and, whenever an uninformed node has an informed neighbor, it becomes informed itself at the next time step), it has been shown that evolving graphs can exhibit communication properties which are much stronger than static networks. In this course, we will first review several results concerning the completion time of rumor spreading in the case of static networks. We will then present some results concerning the completion time of the flooding protocol, which have been obtained in the case of some interesting graph evolution models. Finally, we will present very recent results concerning the completion time of the push version of rumor spreading in the case of dynamic graphs.