PRESENTAZIONE

L'insegnamento fornisce un'introduzione ai principi e all'uso dei metodi formali per garantire la correttezza dei sistemi software.

OBIETTIVI E CONTENUTI

OBIETTIVI FORMATIVI

L'insegnamento offre un'introduzione alle tecniche formali, basate sulla logica, volte a garantire la correttezza dei sistemi software. Si propone di fornire agli studenti la capacità di (a) padroneggiare i concetti e i risultati fondamentali delle teorie dei tipi, comprendendone la connessione con la logica attraverso la corrispondenza tra prove e programmi, (b) acquisire i concetti e i risultati fondamentali del model checking, comprendendo le nozioni di modello, specifica e algoritmo di verifica, (c) utilizzare sistemi di tipi avanzati per sviluppare programmi corretti per costruzione, (d) applicare logiche temporali (lineari e ramificate) per la specifica e la verifica di sistemi software, (e) valutare criticamente quando applicare metodi formali e come questi si integrano con altre tecniche.

OBIETTIVI FORMATIVI (DETTAGLIO) E RISULTATI DI APPRENDIMENTO

Al termine dell'insegnamento, gli studenti saranno in grado di:

- comprendere e ragionare su modelli formali della sintassi, della semantica e dei sistemi di tipo per linguaggi funzionali
- comprendere la connessione tra logica e linguaggi di programmazione tramite la corrispondenza tra prove e programmi
- utilizzare un linguaggio funzionale con tipi dipendenti come proof assistant per scrivere prove formali verificate al calcolatore
- scrivere programmi corretti per costruzione in un linguaggio funzionale con tipi dipendenti
- descrivere il processo generale di model checking
- utilizzare modelli per descrivere il comportamento di un sistema
- comprendere la sintassi e la semantica di diverse logiche temporali a tempo lineare e ramificato e utilizzarle per scrivere specifiche formali
- eseguire algoritmi di model checking per verificare se un sistema soddisfa la sua specifica, anche utilizzando tool dedicati

PREREQUISITI

L'insegnamento non prevede prerequisiti specifici. È utile una certa familiarità di base con i seguenti argomenti: logica proposizionale, linguaggi formali (espressioni regolari e automi a stati finiti), (in)decidibilità dei problemi, complessità spaziale e temporale.

MODALITA' DIDATTICHE

Lezioni frontali e esercitazioni pratiche

PROGRAMMA/CONTENUTO

Parte 1: Teoria dei Tipi
- Elementi di un linguaggio di programmazione: sintassi, semantica e sistema di tipi
- Lambda-calcolo come linguaggio funzionale: termini, riduzione, confluenza e normalizzazione
- Tipi semplici: tipi funzione, prodotto e somma
- Progress, subject reduction e type soundness
- Logica proposizionale intuizionista: proof system, , interpretazione BHK e corrispondenza propositions-as-types/proofs-as-programs
- Normalizzazione forte e coerenza
- Tipi dipendenti: somme e prodotti dipendenti, tipi identità
- Tipi induttivi, pattern matching e ricorsione
- Uso di Agda come linguaggio di programmazione e come proof assistant

Parte 2: Model Checking
- Sistemi di transizione e prodotto di sistemi di transizione
- Proprietà a tempo lineare
- Safety e Liveness
- Automi di Büchi
- Verifica di proprietà regolari e omega-regolari
- Linear Temporal Logic (LTL)
- Model checking per LTL
- Computational Tree Logic (CTL)
- Model checking per CTL
- Uso del model-checker PRISM

TESTI/BIBLIOGRAFIA

- Materiale fornito dai docenti
- J.Y. Girard, Y. Lafont, P. Taylor. *Proofs and Types*. Cambridge University Press, 1989.
- M.H.B. Sorensen, P. Urzyczyn. *Lectures on the Curry-Howard Isomorphism*. Elsevier, 2006.
- J.-P. Katoen, C. Baier. *Principles of Model-Checking*. The MIT Press. 2008.

DOCENTI E COMMISSIONI

LEZIONI

INIZIO LEZIONI

In accordo con il calendario approvato dal Consiglio di Corso di Studi.

Orari delle lezioni

L'orario di questo insegnamento è consultabile all'indirizzo: Portale EasyAcademy

ESAMI

MODALITA' D'ESAME

Esame scritto e orale

MODALITA' DI ACCERTAMENTO

La prova scritta verifica la capacità dello studente di mettere in pratica i concetti visti durante il corso. La prova orale verifica la comprensione dei concetti e la capacità di illustrarli in modo appropriato.