Corso di METODI FORMALI DELL'INFORMATICA 1
Laurea in Informatica
A.A. 2002/2003, 2003/2004, 2004/2005, 2005/2006, 2006/2007
LUCIDI DELLE LEZIONI:
- Introduzione alla verifica formale della
correttezza di programmi.
- Sintassi e semantica operazionale di
programmi deterministici.
- Asserzioni, formule per la correttezza,
nozione di sostituzione di varaibiali in espressioni e asserzioni.
- Sistema di regole alla Hoare per la
correttezza di programmi
deterministici. Esempi.
- Esercizi. Completezza dei sistemi PD e TD.
- 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: correttezza del programma
FINDPOS. Programmi paralleli con sincronizzazione: sintassi,
semantica operazionale.
- Verifica di correttezza di programmi paralleli con sincronizzazione.
- Programmi paralleli con sincronizzazione: produttori e consumatori.
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.