Inizio della pagina -
Logo DISCO
|
Visita la Versione ad elevata leggibilità
|
Vai al Contenuto della pagina
|
Vai alla Fine dei contenuti
|
Vai al Menu Principale
|
Vai alla Barra di navigazione (sei in)
|
Vai al Menu di navigazione (albero)
|
Vai alla Lista dei comandi
|
Vai alla Lista degli approfondimenti
|
Vai al Menu inferiore
|
Logo Ateneo
   
Didattica
Tecniche di analisi e di verifica

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.

 

 

Approfondimenti

Google Translate
Translate to English Translate to French Translate to German Translate to Spanish Translate to Chinese Translate to Portuguese Translate to Arabic
Translate to Albanian Translate to Bulgarian Translate to Croatian Translate to Czech Translate to Danish Translate to Dutch Translate to Finnish Translate to Greek Translate to Hindi
Translate to Hungarian Translate to Irish Translate to Japanese Translate to Korean Translate to Norwegian Translate to Polish Translate to Romanian Translate to Russian Translate to Serbian
Translate to Slovenian Translate to Swedish Translate to Thai Translate to Turkish

(C) Copyright 2016 - Dipartimento Informatica Sistemistica e Comunicazione - Viale Sarca, 336
20126 Milano - Edificio U14
redazioneweb@disco.unimib.it - ultimo aggiornamento di questa pagina 28/03/2011