Docenti: P. Bonizzoni, L. Pomello, F. Cardone
Crediti: 12 CFU
OBIETTIVI FORMATIVI
Conoscenze e abilità.
Il corso si propone di introdurre lo studente alle principali tecniche che consentono di specificare, verificare ed analizzare il comportamento di sistemi a diversi livelli di complessità, ed inoltre agli aspetti algoritmici di questi sistemi.
In particolare, l’interesse del corso è principalmente rivolto all’acquisizione delle necessarie tecniche algoritmiche, logiche e di specifica formale.
Il corso introduce metodi algoritmici utilizzati in applicazioni moderne (quali il web e la Bioinformatica) e i modelli di calcolo basati sulla logica e sulla teoria dei sistemi distribuiti e concorrenti che intervengono nell’analisi e nella verifica di tali applicazioni.
Abilità specifiche acquisite nei tre differenti moduli in cui si articola il corso sono:
- sapere progettare ed analizzare algoritmi evoluti per la soluzione di problemi applicativi,
- sapere modellare e verificare sistemi concorrenti e distribuiti,
- sapere utilizzare tecniche e nozioni legate alla riscrittura e alla logica equazionale, specialmente nell'ambito della specifica e verifica di programmi.
Modulo Analisi di Algoritmi – 4 CFU
Tecniche di analisi degli algoritmi. Algoritmi su grafi.
Algoritmi di approssimazione per problemi NP-difficili e accenni agli algoritmi probabilistici e randomizzati
Applicazioni di algoritmi. I contenuti di questa parte vengono proposti in modo alternato di anno in anno e riguardano applicazioni di algoritmi per l’indicizzazione di documenti, algoritmi per il WEB:
a) algoritmi per la clusterizzazione di dati, la compressione dei dati, strutture dati di indicizzazione: trie, suffix tree e suffix array,
b) algoritmi per motori di ricerca.
Modulo Modelli per la Concorrenza – 4 CFU
Modelli di sistemi concorrenti: classi di reti di Petri, dalle reti Elementari alle reti ad alto livello.
Reti stocastiche e reti temporizzate.
La sintesi dei sistemi PT.
Modelli e proprietà di comportamento.
Verifica di proprietà: metodi strutturali, tecniche di algebra lineare, regole di riduzione, sifoni e trappole, analisi di sottoclassi.
Metodi basati sullo spazio degli stati e Model Checking.
Equivalenza all'osservazione per la verifica di consistenza tra una specifica e un'implementazione.
Modulo Tecniche di Specifica e Dimostrazione – 4 CFU
Segnature del prim’ordine, ad una o più sorta di variabili;
La nozione di algebra per una segnatura ed algebre iniziali;
Generatori di un'algebra, variabili;
Termini e sostituzioni;
Logica equazionale;
Unificazione e pattern matching con gli algoritmi classici;
Regole di riscrittura;
Sistemi di riscrittura canonici e ortogonali;
Confluenza e terminazione;
Tecniche di induzione e ricorsione;
Strategie di riduzione;
Programmazione mediante equazioni: introduzione ai linguaggi funzionali.