Docenti

Prof. Giovanna D'Agostino giovanna.d'agostino@uniud.it
Prof. Marina Lenisa marina.lenisa@uniud.it sito web

Crediti

12 CFU

Finalità

Il corso è diviso in 2 parti: Logica e Metodi Formali.

L'obiettivo del modulo di Logica e`di fornire competenze teoriche e metodologiche in aree d'intersezione fra la Logica Matematica e l' Informatica Teorica, come la Teoria dei Giochi e i Calcoli Logici.

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. 


Programma

Logica:

La prima parte del modulo si occupa dei legami fra l'espressività` di un linguaggio formale e la Teoria dei Giochi, introducendo i giochi di Eherenfeucht per la Logica al Prim'ordine e per la Logica Monadica. In seguito viene introdotto il concetto di bisimulazione e viene brevemente discussa la sua importanza nella modellizzazione dei sistemi informatici;si studiano i rapporti fra le logiche classiche (Logica al prim'ordine e Logica Monadica al second'ordine) ed i loro frammenti invariati per bisimulazione (la logica Modale ed il mu-calcolo). Infine si considera il legame fra giochi infiniti ed il mu-calcolo. Nella seconda parte del modulo si considerano calcoli per la Logica del Prim'ordine che sono alla base della ricerca automatica delle dimostrazioni. In particolare, si studia il metodo di Risoluzione ed il calcolo dei Sequenti.

Metodi Formali:
- Introduzione alla verifica formale della correttezza di programmi.
- Sintassi e semantica operazionale di programmi deterministici.
- Asserzioni, formule per la correttezza, nozione di sostituzione di variabili in espressioni e asserzioni.
- Sistema di regole alla Hoare per la correttezza di programmi deterministici. Esempi.
- Esercizi. Completezza dei sistemi di regole alla Hoare.
- Sintassi e Semantica Operazionale di programmi paralleli disgiunti. 
- 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. Esempi. 
- Correttezza totale di programmi paralleli con variabili condivise.
- Programmi paralleli con variabili condivise: il programma FINDPOS. 
- Programmi paralleli con sincronizzazione: sintassi, semantica operazionale.
- Verifica di correttezza di programmi paralleli con sincronizzazione. 
- Programmi paralleli con sincronizzazione: produttore e consumatore. 
- 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. Esercizi. 
- Introduzione alla programmazione distribuita. Programmi distribuiti: sintassi, semantica operazionale, esempi. Traduzione di programmi distribuiti in programmi non-deterministici. 
- Programmi distribuiti: Teorema di Sequenzializzazione. Verifica: correttezza parziale, correttezza totale debole, correttezza totale. 
- Fairness. 

Bibliografia

Logica:

- Dispense " Introduction to Ehrenfeucht-Fraisse Games" di Kees Doets,
- Dispense del docente;
- materiale tratto da L. Libkin "Finite Model Theory ", Springer
- materiale tratto da A. Asperti, A. Ciabattoni, Logica a Informatica, Mc Graw-Hill

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 orale della parte di Metodi è facoltativa.