Anno di corso: 1

Anno di corso: 2

Crediti: 6
Crediti: 6
Crediti: 6
Tipo: A scelta dello studente
Crediti: 12
Tipo: A scelta dello studente
Crediti: 33
Tipo: Lingua/Prova Finale

MODELLI E COMPUTAZIONE

Scheda dell'insegnamento

Anno accademico di regolamento: 
2018/2019
Anno di corso: 
1
Anno accademico di erogazione: 
2018/2019
Tipo di attività: 
Obbligatorio
Lingua: 
Italiano
Crediti: 
12
Ciclo: 
Primo Semestre
Ore di attivita' didattica: 
106
Prerequisiti: 

Nozioni di base di programmazione imperativa; nozioni di base di logica proposizionale.

*********

Moduli

Metodi di valutazione

Tipo di esame: 
Orale
Modalita' di verifica dell'apprendimento: 

La valutazione di questo modulo comprende una prova scritta con esercizi su tutte le parti del programma, e un colloquio, con discussione della prova scritta e domande sugli argomenti del modulo.

*****************

Prova scritta ed orale. La prova scritta consiste nello svolgimento di esercizi relativi all'acquisizione di competenze specifiche nelle tematiche principali del programma del corso. La prova orale invece è una discussione della parte scritta.

Valutazione: 
Voto Finale

Obiettivi formativi

Acquisire la capacità di modellare e analizzare formalmente sistemi concorrenti; acquisire la capacità di esprimere in linguaggi logici proprietà dei sistemi concorrenti.

********

Teoria della Computazione ha come obiettivo l'acquisizione di strumentalità di base dell'informatica volte alla comprensione della complessità computazionale dei problemi, alla loro classificazione e alle metodologie algoritmiche per la loro soluzione. Inoltre, si intendono fornire capacità in merito alla soluzione di problematiche teoriche poste dalle nuove tecnologie (web, dati massivi, reti complesse, etc.) mediante strutture dati recentemente proposte.

Contenuti

Strumenti teorici per comprendere e manipolare concetti di base dell'informatica relativi al comportamento e alla descrizione di processi distribuiti e concorrenti. Nozioni fondamentali per la verifica di proprietà di programmi e di modelli di sistemi.

*******

Nozioni di base di teoria della computazione (decidibilità, intrattabilità, riduzioni). Classificazione dei problemi in funzione della complessità computazionale. Complessità di approssimazione e parametrica. Approcci moderni per la gestione, indicizzazione, compressione di dati massivi sia con strutture dati che con tecniche algoritmiche innovative. Strutture dati succinte (FM-index), indicizzazione e ricerca per i big-data con tecniche di hashing probabilistico, algoritmi di compressione dati.

Programma esteso

Modelli formali per la specifica e la verifica di correttezza dei programmi. La
semantica assiomatica dei programmi sequenziali, la logica di Hoare.
Modelli della concorrenza: modelli di sistemi reattivi, calcoli di
processi (CCS, Calculus of Communicating Systems) e reti di Petri.
Semantica interleaving (sistemi di transizioni) e a ordini
parziali (reti di Petri) di sistemi concorrenti. Semantica osservazionale e bisimulazione.
La specifica di proprietà e la loro verifica (logiche modali e temporali, algoritmi di model-checking).

*****************

1 Nozioni di base di teoria della computazione (decidibilità, intrattabilità, riduzioni). Classificazione dei problemi in funzione della complessità computazionale. Complessità di approssimazione.

2 Approcci moderni per la gestione, indicizzazione, compressione di grandi mole di dati, sia con strutture dati che con tecniche algoritmiche avanzate.

3 Strutture dati di indicizzazione (es. FM-index, bloom filters, hashing), pattern matching, paradigma shift-And, compressione dati LZ, strutture dati succinte.

4 Applicazioni ed esemplificazioni all'analisi di big-data.

Bibliografia consigliata

Dispense e articoli pubblicati sul sito dell'insegnamento. Testi di consultazione indicati sul sito dell'insegnamento.

***************

Dispense e slides del docente

Metodi didattici

Lezioni frontali (3 CFU, 24 ore) e esercitazioni in aula (3 CFU, 30 ore).

********

Lezione frontale ed esercitazioni