Phd courses 2014

Logic, Sets, and Graphs

Title: Logic, Sets, and Graphs

Lecturer: Alberto Policriti

Period: 15/16/17/18/19 and 22/23/24 September

Sala Seminari Est: 9-11

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

Title: The proof theoretic foundation of computational logic

Lecturer: Dale Miller

Period: April 10-16, Seminari Est, 11-13

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

Title: Probabilistic approaches to the protection of confidential information

Lecturer: Catuscia Palamidessi

Period: April 14,15 Seminari Est, 15-17; April16 Seminari Est 9-11; April 17,18 Seminari Est 11-13

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

Title: Algorithms for big data

Lecturers:  Paolo Ferragina and Andrea Marino

Period: First 5 lectures: 18, 19, 20, 25, 26 november, 9-11, sala seminari EST
Last 4 lectures: 18 March, 15 – 17 Sala Gerace;  20 March, 11-13, sala seminari EST; 25 March, 15 – 17,  Sala Seminari OVEST; 27 March, 11 – 13, Sala Seminari EST.


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

Title: A Framework for Exploring Biology

Lecturer: Prof. Dr. Grzegorz Rozenberg

Period: June 16 – June 27, 2014  — Sala riunioni Ovest: 11-13

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

  1. 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.
  2. 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

Title: Computer-aided cryptography

Lecturer: Dr. Gilles Barthes

Period: May 28: 16-18;  29, 30:  9-12 / June 3,4,5,6: 9-12 / Sala Seminari W

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.

Tentative schedule (2 hours each)

Lecture 1: Introduction

Lecture 2: Provable security (security definitions, assumptions, game-based technique)

Lecture 3: Probabilistic programs (syntax, semantics, probabilistic Hoare logic)

Lecture 4: Relational Hoare Logic

Lecture 5: Advanced verification techniques (eager/lazy sampling, modular proofs, hybrid arguments)

Lecture 6: Padding-based encryption schemes (automated proofs, synthesis, symbolic attack discovery)

Lecture 7: Cryptographic implementations (side-channel attacks, verified C implementations, code generation)

Lecture 8: Key-exchange protocols (models, formalization, NAXOS)

Lecture 9: Differential privacy

Lecture 10: Higher-order programs

Specification methods

Title: Specification methods

Lecturer: Egon Börger

Period: 13-31 January 2014


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

Other courses

In addition, each student can attend a course of the Master programme in Computer Science, for instance: