Sign In


Sort by AttachmentsUse SHIFT+ENTER to open the menu (new window).
Calculus of Computation: Decision procedures with applications to analyzing and developing robust software.Use SHIFT+ENTER to open the menu (new window).
Zohar Manna September - 8th October --- All lectures will be at 11-13 in Sala Seminari W

Foundation: Logic review. Propositional and first-order logic; induction.
Verification: Methods for proving correctness of sequential programs using first-order reasoning; need for decision procedures.
Decision procedures: Algorithms that decide the validity of logical formulas for common theories including SAT, equality, arithmetic, recursive data structures, and arrays. Combination theories and combination of decision procedures.

Materials: The Calculus of Computation: Decision Procedures with Applications to Verification by A.Bradley and Z.Manna, Springer 2007
Privacy and anonymity in location- and movement-aware data analysis Use SHIFT+ENTER to open the menu (new window).
Fosca Giannotti, Dino Pedreschi, Franco Turini KDD Lab Università di Pisa and ISTI-CNR, Pisa, ItalyJune 15-July 17 --- all lectures will be in Sala Seminari W

The course shall focus on the issue of privacy and anonymity in location-aware and movement-aware data, presenting an original account of the newly emerging and active research areas of:
* privacy and anonymity in location-based services: models of location-privacy that support anonymity of mobile users during real-time service;
* privacy and anonymity in mobility data analysis: models of privacy and anonymity threats for mobility data publishing and mobility data mining, and related privacy-preserving techniques for secure mobility data publishing and secure mobility data mining.

Materials: Fosca Giannotti, Dino Pedreschi (Eds.) Mobility, Data Mining and Privacy, LNCS Springer, 2007
Web search (in two parts)Use SHIFT+ENTER to open the menu (new window).
S. Muthukrishnan                       and           Aristides Gionis part: June - 2nd part Winter

Theory of Sponsored Search Auctions
S. Muthukrishnan, Google Inc.

Web search engines are becoming an increasingly important advertising medium. When a user poses a query, in addition to search results, the search engine also returns a few advertisements. On most major search engines, the choice and assignment of ads to positions is determined by an auction among all advertisers who placed a bid on some keyword that matches the query. The user might click on one or more of the ads, in which case (in the pay-per-click model) the advertiser receiving the click pays the search engine a price determined by the auction. While economic and game theory provide a well-developed framework for understanding auctions in general, the particular instance of sponsored search auctions presents new challenges.
In traditional auctions, the auctioneer and the buyers are the only active players, with the commodity being inert. Here, the value of the commodity itself is determined by the behavior of search engine users which introduces complications. Further, different advertisers and users have widely different goals and behavior, so simple utility models may not capture the hybrid mix of these players in the auction.
Also, the game consists of not just a single auction, or even several repeated auctions, but rather a portfolio of auctions that are run corresponding to the entire ensemble of user queries. In presence of budgets, a study of such a portfolio of auctions becomes challenging. Finally, the scale of this operation with billions of events a day brings focus on computational challenges, more so than in most auction scenarios.
This course will cover the theory behind the auction for a single user query. This part of the course will discuss classical auction theory, the new concepts and techniques developed to understand the current sponsored search auctions, and discuss some open issues as we attempt to generalize these auctions. In the second part, we take a more global view and discuss auctions for the ensemble of user queries. Many optimization issues are involved, and the tutorial will discuss the basic theory here. Finally, we will discuss some new directions and open problems.

Topics in web mining and next-generation search
Aris Gionis, Yahoo! Research.

In the classic paradigm of Internet, there is a clear distinction between the users who publish content and those users who search for information. Evolving from this classic paradigm, the Internet is becoming a medium for establishing social connections, publishing information in a cooperative manner, making economic transactions, sharing experiences, and being entertained. In this new social environment the borders between information producers and information consumers are becoming increasingly fuzzy. Searching for information in this new environment creates a new information-search paradigm that offers more capabilities and allows users to find high quality information tailored to their needs. On the other hand, the volume and heterogeneity of the available data makes the search problem considerably more challenging.
Another very important and rich source of web data, which complement content data, are access logs. Dealing with access logs can be a very challenging task due to the extremely large volume of the data and the presence of noise. On the other hand, access logs are very valuable because they record direct information about the interests of users and their feedback in the system. Thus, mining access logs can provide very useful cues about user behavior, it can help extracting latent knowledge such as folksonomies, and it may be used to improve web applications.
In this course we will present selected topics and discuss recent research papers in the above areas of web mining, namely mining query logs and user-generated content.

Structural Operational SemanticsUse SHIFT+ENTER to open the menu (new window).
Simone Tini, Università dell'InsubriaJuly 6-16 -- all lectures are in Sala Seminari W, 11-13

Description: Structural Operational Semantics (SOS) provides a framework to give an operational semantics to programming and specification languages. In particular, concurrent process calculi are usually equipped with an SOS. The idea of SOS is to generate Labeled Transition Systems (LTSs) from Transition System Specifications (TSSs), namely sets of Transition Rules of the form premises/conclusion, which describe how moves of a process can be inferred from moves of its subprocesses.

1. Preliminaries.
* Labeled Transition Systems,
* Behavioral Equivalences and Preorders,
* Term Algebras,
* Transition System Specifications.

2. The meaning of Transition System Specifications. Associating an LTS with a TSS is not immediate if "negative premises" appear in the transition rules. Several approaches have been proposed.
* Model-Theoretic Approach,
* Proof-Theoretic Approach,
* Stratification-Based Approach.

3. Conservative Extensions. When a language equipped with an SOS is extended with new features, are we sure that all processes specified with the original language keep the same behavior? The notion of Conservative Extension is an answer to this question.
* Operational Conservative Extension,
* Applications to Axiomatizations,
* Applications to Rewriting.

4. Congruence Formats. Instead of proving a result for a given language, one can attempt to establish results holding for classes of languages. The idea behind the notion of "format" is that the languages are classified on the basis of the syntactic form of the transition rules.
* Panth Format for bisimulation,
* Ntree Format,
* De Simone Format and De Simone Languages,
* GSOS Format,
* RBB Safe Format for weak bisimulation,
* Precongruence Formats for Behavioral Preorders.

5. Non classic SOS. Applications of SOS theory to probabilistic languages and to the non interference security property are showed.
* Rule Formats for Non-Interference.
* Rule Formats for Probabilistic Languages.

Fondamenti di LogicaUse SHIFT+ENTER to open the menu (new window).
Simone Martini May-June
Sistemi in deduzione naturale e a sequenti per la logica classica e intuizionista. Relazioni tra i due.
- Teoria della dimostrazione: eliminazione del taglio e/o normalizzazione. Consequenze.

Qualche argomento a scelta tra i seguenti:
- Lambda-calcolo tipizzato e la corrispondenza di Curry-Howard. Normalizzazione forte; Confluenza.
- Logica lineare: sequenti, reti di dimostrazioni. Cenni alla semantica Logiche leggere e relazioni con la complessita' computazionale implicita
- Logiche modali classiche: semantica, modelli di Kripke, relazione di accessibilita'.

Il docente e` disponibile a trattare i classici teoremi limitativi (Goedel, Church, Tarski), nel caso in cui l'uditorio ne avesse necessita`.
Biological Sequence AnalysisUse SHIFT+ENTER to open the menu (new window).
Esko Ukkonen University of Helsinki 28 -- Oct. 8

Computational analysis of biological sequences (DNA, RNA, protein sequences) is in the core of bioinformatics. The course will give an introduction to the computational toolbox in the area. The emphasis will be on algorithms, and the approach is a mixture of probabilistic and combinatorial techniques. In addition to the classic algorithms for pairwise and multiple alignments and for database searches also some novel topics on high-throughput sequencing, gene regulatory motifs and haplotypes will be covered.

Contents (tentative)
- biological sequences
- probabilistic models of sequences
Pairwise alignment - motivation
- scoring schemes: BLOSUM etc
- global alignment: Needleman-Wunsch algorithm
- local alignment: Smith-Waterman algorithm
- significance of alignment scores: Karlin-Altschul statistics
Similarity searches in databases
- basic dynamic programming
- heuristic improvements: Blast
- index-based approach: dynamic programming over suffix tree
The fragment assembly problem
- the classic three-step algorithm
- practical improvements
- implications of the new high-throughput sequencing technologies
Multiple alignment
- scoring schemes
- basic solution by dynamic programming
- some heuristic improvements
Hidden Markov Models (HMMs) for sequence families
- HMM definition and basic techniques (Viterbi, Forward)
- building multiple alignments
- HMM learning using EM algorithm
Sequence motifs for transcription factor binding
- families of motifs
- suffix-tree techniques for substring motifs
- position weight matrix (PWM)
- learning PWMs with EM from high-throughput data
Fast search methods for PWMs
- significance thresholding
- naive algorithm
- more advanced algorithms
Gene regulatory motifs
- gene regulatory elements in DNA
- predicting putative elements: the EEL algorithm
The haplotyping problem (if time allows)
- genotypes and haplotypes
- HMM approach to haplotyping

Packing and cutting problemsUse SHIFT+ENTER to open the menu (new window).
Valerio De Carvalho
April 20 - 24
Teoria dell'Informazione (undergraduate course)Use SHIFT+ENTER to open the menu (new window).
Francesco Romani2nd academic semester
Tecniche di specifica e dimostrazione (undergraduate course)Use SHIFT+ENTER to open the menu (new window).
Ugo Montanari2nd academic semester
Topics in Integer ProgrammingUse SHIFT+ENTER to open the menu (new window).
J.M. Valério de Carvalho to be defined