Metodi formali e logica per l'informatica - Formal Methods and Logic for Computer Science
Docente
- Prof. Giovanna D'Agostino
- Prof. Marina Lenisa
Indirizzo e-mail
Indirizzo Pagina Web Personale
http://people.uniud.it/page/giovanna.dagostino
http://www.dimi.uniud.it/members/marina.lenisa/
Crediti
12 CFU
Finalità e obbiettivi formativi
Il corso e` diviso in 2 parti: Logica e Metodi Formali.
L'obiettivo del modulo di logica è quello di fornire un ampio panorama del ruolo della Logica nelle sue aree d'intersezione con l'Informatica, quali la Teoria dei Giochi, la Verifica dei Sistemi e l'Intelligenza Artificiale.
L'obiettivo del modulo di Metodi Formali e` quello di fornire allo studente strumenti rigorosi per la verifica formale di correttezza di programmi. In particolare, verra` illustrata la Logica di Hoare, basata su invarianti, per la verifica di programmi sequenziali, paralleli e distribuiti. Si discuteranno formalmente correttezza e terminazione di diversi algoritmi sequenziali classici. Mentre questioni come assenza di deadlock e fairness verranno affrontate formalmente per una serie di problemi paradigmatici di concorrenza.
Programma
Logica:
-LOGICA E GIOCHI.
- Definizione matematica di gioco. Strategie. Determinatezza.
- Giochi di Ehrenfeucht ed espressività della Logica al Prim'ordine.
-LOGICA E VERIFICA
- Superamento della logica al prim'ordine: S1S, Automi di Buchi e Giochi. - Riscoperta della logica modale: Bisimulazione. Logiche Temporali (cenni).
-LOGICA E INTELLIGENZA ARTIFICIALE
- Logiche Epistemiche e Descrittive.
- Ragionamento non monotono.
Metodi Formali:
- Introduzione alla verifica formale della correttezza di programmi.
- Sintassi e semantica operazionale di programmi deterministici.
- Sistema di regole alla Hoare per la correttezza di programmi deterministici. -Verifica formale di algoritmi sequenziali classici. Correttezza parziale e terminazione.
- Completezza dei sistemi di regole alla Hoare.
- Sintassi e Semantica Operazionale di programmi paralleli disgiunti.
- Riduzione del parallelismo disgiunto alla sequenzialita`.
- Verifica di programmi paralleli disgiunti.
- Verifica di programmi paralleli con variabili condivise: correttezza parziale.
- Correttezza Forte dei proof outline. Regola per il parallelismo e sua incompletezza. Regola per le variabili ausiliarie.
- Correttezza totale di programmi paralleli con variabili condivise.
- Programmi paralleli con variabili condivise. Comportamento non-composizionale delle componenti.
- Programmi paralleli con sincronizzazione: sintassi, semantica operazionale.
- Verifica di correttezza di programmi paralleli con sincronizzazione: correttezza parziale, terminazione, assenza di deadlock.
- Verifica di correttezza di esempi classici di programmi paralleli con sincronizzazione: produttore e consumatore, lettori e scrittori, implementazione e uso di semafori, etc.
- Programmi non-deterministici: sintassi, semantica operazionale, regole per la verifica di correttezza.
- Utilità dei programmi non-deterministici. Traduzione di programmi paralleli in programmi non-deterministici.
- Introduzione alla programmazione distribuita. Programmi distribuiti: sintassi, semantica operazionale.
- Esempi classici: il problema della trasmissione nelle sue varianti (con e senza filtraggio di dati, con e senza messaggi di acknowledgment, etc).
- Traduzione di programmi distribuiti in programmi non-deterministici e relazioni tra le semantiche.
- Verifica: correttezza parziale, terminazione, assenza di deadlock.
- Fairness: studio della correttezza di programmi paralleli sotto l'ipotesi di schedulazione fair. La metodologia presentata si basa sull'implementazione di uno scheduler fair all'interno del programma stesso. Tale implementazione e` definita su un linguaggio esteso con assegnamento random. La prova di terminazione richiede l'utilizzo di funzioni di terminazione definite su strutture ben fondate che generalizzano i naturali.
Prerequisiti
Logica:
Conoscenza di base della sintassi e della semantica della Logica Proposizionale e della Logica al Prim'ordine.
(vedere ad esempio http://users.dimi.uniud.it/~alberto.marcone/dispenseLM1314.pdf ed in particolare i capitoli 1,2,3,6,7,8,9)
Metodi formali:
Programmazione e laboratorio (necessario).
Logica Matematica (necessario)
Sistemi Operativi (necessario)
Bibliografia
Logica:
Appunti ed articoli forniti durante il corso. Gli studenti non frequentanti possono
reperire tale materiale sul materiale didattico di ateneo.
Metodi Formali:
- Trasparenze usate a lezione
- Apt K., de Boer F., Olderog E-R., "Verification of Sequential and Concurrent Programs", Springer, 3rd edition, 2009.
Modalità d'esame
L'esame è costituito da una prova scritta ed una orale.
La prova scritta e la prova orale sono costituite da due parti: Logica e Metodi Formali.
La prova scritta di Logica consiste nello svolgimento di esercizi.
La prova orale di Metodi è facoltativa.
Il voto finale è la media (arrotondata per eccesso) dei voti nelle due parti.
Gli studenti che hanno frequentato il corso con un programma differente da quello descritto potranno svolgere l'esame su tale programma, previa comunicazione al docente almeno una settimana prima della data di svolgimento dello scritto.
Orario di ricevimento
Logica:
Su appuntamento, inviando una mail a giovanna.dagostino@uniud.it
Metodi formali:
Lunedì 10.00-11.00 oppure su appuntamento.