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.