– 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.

– Utilita` 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.