Università degli Studi di Perugia

Prova orale e scritta (prova scritta eventualmente sostituibile da prova pratica)

.

.

.

Introduzione e concetti preliminari.
Semantica dei programmi deterministici. Programmi ricorsivi.
Programmi paralleli disgiunti.
Programmi paralleli con memoria condivisa e con sincronizzazione.
Cenni ai casi dei programmi nondeterministici, distribuiti.
Cenni al trattamento dei programmi orientati agli oggetti.

Introduzione e concetti preliminari. Semantica dei programmi deterministici. Programmi ricorsivi.
Programmi paralleli disgiunti.
Programmi paralleli con memoria condivisa e con sincronizzazione.
Cenni ai casi dei programmi nondeterministici, distribuiti.
Cenni al trattamento dei programmi orientati agli oggetti.

Lezioni frontali

Verification of Sequential and Concurrent Programs. K. R. Apt, F. S. de Boer, E.-R. Olderog, Springer 2010. Terza edizione.
La semantica formale dei linguaggi di programmazione, Winskel, UTET/MIT-press, 1999. (anche in inglese:The Formal Semantics of Programming Languages MIT-press).
Materiale aggiuntivo fornito dal docente.

Il corso si propone di fornire le nozioni alla base dell'analisi e la verifica formale/automatica del software.
Lo studente acquisirà le competenze necessarie ad applicare tecniche formali per l'analisi di programmi, la comprensione del loro comportamento, la loro progettazione, la verifica e la certificazione di proprietà di programmi (sia sequenziali che paralleli).

primo semestre 2013-14

.

.

facoltativa

Dip. di Matematica e Informatica

.